Documentation

Mathlib.Data.Fintype.Sigma

fintype instances for sigma types #

theorem Set.biUnion_finsetSigma_univ {ι : Type u_1} {α : Type u_2} {κ : ιType u_3} [(i : ι) → Fintype (κ i)] (s : Finset ι) (f : Sigma κSet α) :
ijs.sigma fun (x : ι) => Finset.univ, f ij = is, ⋃ (j : κ i), f i, j
theorem Set.biUnion_finsetSigma_univ' {ι : Type u_1} {α : Type u_2} {κ : ιType u_3} [(i : ι) → Fintype (κ i)] (s : Finset ι) (f : (i : ι) → κ iSet α) :
is, ⋃ (j : κ i), f i j = ijs.sigma fun (x : ι) => Finset.univ, f ij.fst ij.snd
theorem Set.biInter_finsetSigma_univ {ι : Type u_1} {α : Type u_2} {κ : ιType u_3} [(i : ι) → Fintype (κ i)] (s : Finset ι) (f : Sigma κSet α) :
ijs.sigma fun (x : ι) => Finset.univ, f ij = is, ⋂ (j : κ i), f i, j
theorem Set.biInter_finsetSigma_univ' {ι : Type u_1} {α : Type u_2} {κ : ιType u_3} [(i : ι) → Fintype (κ i)] (s : Finset ι) (f : (i : ι) → κ iSet α) :
is, ⋂ (j : κ i), f i j = ijs.sigma fun (x : ι) => Finset.univ, f ij.fst ij.snd
instance Sigma.instFintype {ι : Type u_1} {κ : ιType u_3} [(i : ι) → Fintype (κ i)] [Fintype ι] :
Fintype ((i : ι) × κ i)
Equations
  • Sigma.instFintype = { elems := Finset.univ.sigma fun (x : ι) => Finset.univ, complete := }
instance PSigma.instFintype {ι : Type u_1} {κ : ιType u_3} [(i : ι) → Fintype (κ i)] [Fintype ι] :
Fintype ((i : ι) ×' κ i)
Equations
@[simp]
theorem Finset.univ_sigma_univ {ι : Type u_1} {κ : ιType u_3} [(i : ι) → Fintype (κ i)] [Fintype ι] :
(Finset.univ.sigma fun (x : ι) => Finset.univ) = Finset.univ