# Finite sets in a sigma type #

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.sigmaLift: Lifts maps α i → β i → Finset (γ i) to a map Σ i, α i → Σ i, β i → Finset (Σ i, γ i).

## TODO #

Finset.sigmaLift 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.

def Finset.sigma {ι : Type u_1} {α : ιType u_2} (s : ) (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
• s.sigma t = { val := s.val.sigma fun (i : ι) => (t i).val, nodup := }
Instances For
@[simp]
theorem Finset.mem_sigma {ι : Type u_1} {α : ιType u_2} {s : } {t : (i : ι) → Finset (α i)} {a : (i : ι) × α i} :
a s.sigma t a.fst s a.snd t a.fst
@[simp]
theorem Finset.coe_sigma {ι : Type u_1} {α : ιType u_2} (s : ) (t : (i : ι) → Finset (α i)) :
(s.sigma t) = (↑s).sigma fun (i : ι) => (t i)
@[simp]
theorem Finset.sigma_nonempty {ι : Type u_1} {α : ιType u_2} {s : } {t : (i : ι) → Finset (α i)} :
(s.sigma t).Nonempty is, (t i).Nonempty
@[simp]
theorem Finset.sigma_eq_empty {ι : Type u_1} {α : ιType u_2} {s : } {t : (i : ι) → Finset (α i)} :
s.sigma t = is, t i =
theorem Finset.sigma_mono {ι : Type u_1} {α : ιType u_2} {s₁ : } {s₂ : } {t₁ : (i : ι) → Finset (α i)} {t₂ : (i : ι) → Finset (α i)} (hs : s₁ s₂) (ht : ∀ (i : ι), t₁ i t₂ i) :
s₁.sigma t₁ s₂.sigma t₂
theorem Finset.pairwiseDisjoint_map_sigmaMk {ι : Type u_1} {α : ιType u_2} {s : } {t : (i : ι) → Finset (α i)} :
(↑s).PairwiseDisjoint fun (i : ι) => Finset.map (t i)
@[simp]
theorem Finset.disjiUnion_map_sigma_mk {ι : Type u_1} {α : ιType u_2} {s : } {t : (i : ι) → Finset (α i)} :
s.disjiUnion (fun (i : ι) => Finset.map (t i)) = s.sigma t
theorem Finset.sigma_eq_biUnion {ι : Type u_1} {α : ιType u_2} [DecidableEq ((i : ι) × α i)] (s : ) (t : (i : ι) → Finset (α i)) :
s.sigma t = s.biUnion fun (i : ι) => Finset.map (t i)
theorem Finset.sup_sigma {ι : Type u_1} {α : ιType u_2} {β : Type u_3} (s : ) (t : (i : ι) → Finset (α i)) (f : (i : ι) × α iβ) [] [] :
(s.sigma t).sup f = s.sup fun (i : ι) => (t i).sup fun (b : α i) => f i, b
theorem Finset.inf_sigma {ι : Type u_1} {α : ιType u_2} {β : Type u_3} (s : ) (t : (i : ι) → Finset (α i)) (f : (i : ι) × α iβ) [] [] :
(s.sigma t).inf f = s.inf fun (i : ι) => (t i).inf fun (b : α i) => f i, b
theorem biSup_finsetSigma {ι : Type u_1} {α : ιType u_2} {β : Type u_3} [] (s : ) (t : (i : ι) → Finset (α i)) (f : β) :
ijs.sigma t, f ij = is, jt i, f i, j
theorem biSup_finsetSigma' {ι : Type u_1} {α : ιType u_2} {β : Type u_3} [] (s : ) (t : (i : ι) → Finset (α i)) (f : (i : ι) → α iβ) :
is, jt i, f i j = ijs.sigma t, f ij.fst ij.snd
theorem biInf_finsetSigma {ι : Type u_1} {α : ιType u_2} {β : Type u_3} [] (s : ) (t : (i : ι) → Finset (α i)) (f : β) :
ijs.sigma t, f ij = is, jt i, f i, j
theorem biInf_finsetSigma' {ι : Type u_1} {α : ιType u_2} {β : Type u_3} [] (s : ) (t : (i : ι) → Finset (α i)) (f : (i : ι) → α iβ) :
is, jt i, f i j = ijs.sigma t, f ij.fst ij.snd
theorem Set.biUnion_finsetSigma {ι : Type u_1} {α : ιType u_2} {β : Type u_3} (s : ) (t : (i : ι) → Finset (α i)) (f : Set β) :
ijs.sigma t, f ij = is, jt i, f i, j
theorem Set.biUnion_finsetSigma' {ι : Type u_1} {α : ιType u_2} {β : Type u_3} (s : ) (t : (i : ι) → Finset (α i)) (f : (i : ι) → α iSet β) :
is, jt i, f i j = ijs.sigma t, f ij.fst ij.snd
theorem Set.biInter_finsetSigma {ι : Type u_1} {α : ιType u_2} {β : Type u_3} (s : ) (t : (i : ι) → Finset (α i)) (f : Set β) :
ijs.sigma t, f ij = is, jt i, f i, j
theorem Set.biInter_finsetSigma' {ι : Type u_1} {α : ιType u_2} {β : Type u_3} (s : ) (t : (i : ι) → Finset (α i)) (f : (i : ι) → α iSet β) :
is, jt i, f i j = ijs.sigma t, f ij.fst ij.snd
def Finset.sigmaLift {ι : Type u_1} {α : ιType u_2} {β : ιType u_3} {γ : ιType u_4} [] (f : i : ι⦄ → α iβ iFinset (γ i)) (a : ) (b : ) :

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

Equations
Instances For
theorem Finset.mem_sigmaLift {ι : Type u_1} {α : ιType u_2} {β : ιType u_3} {γ : ιType u_4} [] (f : i : ι⦄ → α iβ iFinset (γ i)) (a : ) (b : ) (x : ) :
x ∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd f (haa.snd) (hbb.snd)
theorem Finset.mk_mem_sigmaLift {ι : Type u_1} {α : ιType u_2} {β : ιType u_3} {γ : ιType u_4} [] (f : i : ι⦄ → α iβ iFinset (γ i)) (i : ι) (a : α i) (b : β i) (x : γ i) :
i, x Finset.sigmaLift f i, a i, b x f a b
theorem Finset.not_mem_sigmaLift_of_ne_left {ι : Type u_1} {α : ιType u_2} {β : ιType u_3} {γ : ιType u_4} [] (f : i : ι⦄ → α iβ iFinset (γ i)) (a : ) (b : ) (x : ) (h : a.fst x.fst) :
x
theorem Finset.not_mem_sigmaLift_of_ne_right {ι : Type u_1} {α : ιType u_2} {β : ιType u_3} {γ : ιType u_4} [] (f : i : ι⦄ → α iβ iFinset (γ i)) {a : } (b : ) {x : } (h : b.fst x.fst) :
x
theorem Finset.sigmaLift_nonempty {ι : Type u_1} {α : ιType u_2} {β : ιType u_3} {γ : ιType u_4} [] {f : i : ι⦄ → α iβ iFinset (γ i)} {a : (i : ι) × α i} {b : (i : ι) × β i} :
(Finset.sigmaLift f a b).Nonempty ∃ (h : a.fst = b.fst), (f (ha.snd) b.snd).Nonempty
theorem Finset.sigmaLift_eq_empty {ι : Type u_1} {α : ιType u_2} {β : ιType u_3} {γ : ιType u_4} [] {f : i : ι⦄ → α iβ iFinset (γ i)} {a : (i : ι) × α i} {b : (i : ι) × β i} :
= ∀ (h : a.fst = b.fst), f (ha.snd) b.snd =
theorem Finset.sigmaLift_mono {ι : Type u_1} {α : ιType u_2} {β : ιType u_3} {γ : ιType u_4} [] {f : i : ι⦄ → α iβ iFinset (γ i)} {g : i : ι⦄ → α iβ iFinset (γ i)} (h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b g a b) (a : (i : ι) × α i) (b : (i : ι) × β i) :
theorem Finset.card_sigmaLift {ι : Type u_1} {α : ιType u_2} {β : ιType u_3} {γ : ιType u_4} [] (f : i : ι⦄ → α iβ iFinset (γ i)) (a : (i : ι) × α i) (b : (i : ι) × β i) :
(Finset.sigmaLift f a b).card = if h : a.fst = b.fst then (f (ha.snd) b.snd).card else 0