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 α) : ⋃ ij ∈ s.sigma fun (x : ι) => Finset.univ, f ij = ⋃ i ∈ s, ⋃ (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 : ι) → κ i → Set α) : ⋃ i ∈ s, ⋃ (j : κ i), f i j = ⋃ ij ∈ s.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 α) : ⋂ ij ∈ s.sigma fun (x : ι) => Finset.univ, f ij = ⋂ i ∈ s, ⋂ (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 : ι) → κ i → Set α) : ⋂ i ∈ s, ⋂ (j : κ i), f i j = ⋂ ij ∈ s.sigma fun (x : ι) => Finset.univ, f ij.fst ij.snd

@[instance_reducible]

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_reducible]

instance PSigma.instFintype {ι : Type u_1} {κ : ι → Type u_3} [(i : ι) → Fintype (κ i)] [Fintype ι] : Fintype ((i : ι) ×' κ i)

Equations

• PSigma.instFintype = Fintype.ofEquiv ((i : ι) × κ i) (Equiv.psigmaEquivSigma κ).symm

@[simp]

theorem Finset.univ_sigma_univ {ι : Type u_1} {κ : ι → Type u_3} [(i : ι) → Fintype (κ i)] [Fintype ι] : (univ.sigma fun (x : ι) => univ) = univ