# mathlib3documentation

data.finset.sigma

# Finite sets in a sigma type #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines a few finset constructions on Σ i, α i.

## Main declarations #

• finset.sigma: Given a finset s in ι and finsets t i in each α i, s.sigma t is the finset of the dependent sum Σ i, α i
• finset.sigma_lift: Lifts maps α i → β i → finset (γ i) to a map Σ i, α i → Σ i, β i → finset (Σ i, γ i).

## TODO #

finset.sigma_lift can be generalized to any alternative functor. But to make the generalization worth it, we must first refactor the functor library so that the alternative instance for finset is computable and universe-polymorphic.

@[protected]
def finset.sigma {ι : Type u_1} {α : ι Type u_2} (s : finset ι) (t : Π (i : ι), finset (α i)) :
finset (Σ (i : ι), α i)

s.sigma t is the finset of dependent pairs ⟨i, a⟩ such that i ∈ s and a ∈ t i.

Equations
@[simp]
theorem finset.mem_sigma {ι : Type u_1} {α : ι Type u_2} {s : finset ι} {t : Π (i : ι), finset (α i)} {a : Σ (i : ι), α i} :
a s.sigma t a.fst s a.snd t a.fst
@[simp, norm_cast]
theorem finset.coe_sigma {ι : Type u_1} {α : ι Type u_2} (s : finset ι) (t : Π (i : ι), finset (α i)) :
(s.sigma t) = s.sigma (λ (i : ι), (t i))
@[simp]
theorem finset.sigma_nonempty {ι : Type u_1} {α : ι Type u_2} {s : finset ι} {t : Π (i : ι), finset (α i)} :
(s.sigma t).nonempty (i : ι) (H : i s), (t i).nonempty
@[simp]
theorem finset.sigma_eq_empty {ι : Type u_1} {α : ι Type u_2} {s : finset ι} {t : Π (i : ι), finset (α i)} :
s.sigma t = (i : ι), i s t i =
theorem finset.sigma_mono {ι : Type u_1} {α : ι Type u_2} {s₁ s₂ : finset ι} {t₁ t₂ : Π (i : ι), finset (α i)} (hs : s₁ s₂) (ht : (i : ι), t₁ i t₂ i) :
s₁.sigma t₁ s₂.sigma t₂
theorem finset.pairwise_disjoint_map_sigma_mk {ι : Type u_1} {α : ι Type u_2} {s : finset ι} {t : Π (i : ι), finset (α i)} :
s.pairwise_disjoint (λ (i : ι), (t i))
@[simp]
theorem finset.disj_Union_map_sigma_mk {ι : Type u_1} {α : ι Type u_2} {s : finset ι} {t : Π (i : ι), finset (α i)} :
theorem finset.sigma_eq_bUnion {ι : Type u_1} {α : ι Type u_2} [decidable_eq (Σ (i : ι), α i)] (s : finset ι) (t : Π (i : ι), finset (α i)) :
s.sigma t = s.bUnion (λ (i : ι), (t i))
theorem finset.sup_sigma {ι : Type u_1} {α : ι Type u_2} {β : Type u_3} (s : finset ι) (t : Π (i : ι), finset (α i)) (f : (Σ (i : ι), α i) β) [order_bot β] :
(s.sigma t).sup f = s.sup (λ (i : ι), (t i).sup (λ (b : α i), f i, b⟩))
theorem finset.inf_sigma {ι : Type u_1} {α : ι Type u_2} {β : Type u_3} (s : finset ι) (t : Π (i : ι), finset (α i)) (f : (Σ (i : ι), α i) β) [order_top β] :
(s.sigma t).inf f = s.inf (λ (i : ι), (t i).inf (λ (b : α i), f i, b⟩))
def finset.sigma_lift {ι : Type u_1} {α : ι Type u_2} {β : ι Type u_3} {γ : ι Type u_4} [decidable_eq ι] (f : Π ⦃i : ι⦄, α i β i finset (γ i)) (a : sigma α) (b : sigma β) :

Lifts maps α i → β i → finset (γ i) to a map Σ i, α i → Σ i, β i → finset (Σ i, γ i).

Equations
theorem finset.mem_sigma_lift {ι : Type u_1} {α : ι Type u_2} {β : ι Type u_3} {γ : ι Type u_4} [decidable_eq ι] (f : Π ⦃i : ι⦄, α i β i finset (γ i)) (a : sigma α) (b : sigma β) (x : sigma γ) :
x b (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd f (eq.rec a.snd ha) (eq.rec b.snd hb)
theorem finset.mk_mem_sigma_lift {ι : Type u_1} {α : ι Type u_2} {β : ι Type u_3} {γ : ι Type u_4} [decidable_eq ι] (f : Π ⦃i : ι⦄, α i β i finset (γ i)) (i : ι) (a : α i) (b : β i) (x : γ i) :
i, x⟩ i, a⟩ i, b⟩ x f a b
theorem finset.not_mem_sigma_lift_of_ne_left {ι : Type u_1} {α : ι Type u_2} {β : ι Type u_3} {γ : ι Type u_4} [decidable_eq ι] (f : Π ⦃i : ι⦄, α i β i finset (γ i)) (a : sigma α) (b : sigma β) (x : sigma γ) (h : a.fst x.fst) :
x b
theorem finset.not_mem_sigma_lift_of_ne_right {ι : Type u_1} {α : ι Type u_2} {β : ι Type u_3} {γ : ι Type u_4} [decidable_eq ι] (f : Π ⦃i : ι⦄, α i β i finset (γ i)) {a : sigma α} (b : sigma β) {x : sigma γ} (h : b.fst x.fst) :
x b
theorem finset.sigma_lift_nonempty {ι : Type u_1} {α : ι Type u_2} {β : ι Type u_3} {γ : ι Type u_4} [decidable_eq ι] {f : Π ⦃i : ι⦄, α i β i finset (γ i)} {a : Σ (i : ι), α i} {b : Σ (i : ι), β i} :
b).nonempty (h : a.fst = b.fst), (f (eq.rec a.snd h) b.snd).nonempty
theorem finset.sigma_lift_eq_empty {ι : Type u_1} {α : ι Type u_2} {β : ι Type u_3} {γ : ι Type u_4} [decidable_eq ι] {f : Π ⦃i : ι⦄, α i β i finset (γ i)} {a : Σ (i : ι), α i} {b : Σ (i : ι), β i} :
b = (h : a.fst = b.fst), f (eq.rec a.snd h) b.snd =
theorem finset.sigma_lift_mono {ι : Type u_1} {α : ι Type u_2} {β : ι Type u_3} {γ : ι Type u_4} [decidable_eq ι] {f g : Π ⦃i : ι⦄, α i β i finset (γ i)} (h : ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b g a b) (a : Σ (i : ι), α i) (b : Σ (i : ι), β i) :
b b
theorem finset.card_sigma_lift {ι : Type u_1} {α : ι Type u_2} {β : ι Type u_3} {γ : ι Type u_4} [decidable_eq ι] (f : Π ⦃i : ι⦄, α i β i finset (γ i)) (a : Σ (i : ι), α i) (b : Σ (i : ι), β i) :
b).card = dite (a.fst = b.fst) (λ (h : a.fst = b.fst), (f (eq.rec a.snd h) b.snd).card) (λ (_x : ¬a.fst = b.fst), 0)