fintype instances for sigma types #
theorem
Set.biUnion_finsetSigma_univ'
{ι : Type u_1}
{α : Type u_2}
{κ : ι → Type u_5}
[(i : ι) → Fintype (κ i)]
(s : Finset ι)
(f : (i : ι) → κ i → Set α)
:
⋃ i ∈ s, ⋃ (j : κ i), f i j = ⋃ ij ∈ Finset.sigma s fun (x : ι) => Finset.univ, f ij.fst ij.snd
theorem
Set.biInter_finsetSigma_univ'
{ι : Type u_1}
{α : Type u_2}
{κ : ι → Type u_5}
[(i : ι) → Fintype (κ i)]
(s : Finset ι)
(f : (i : ι) → κ i → Set α)
:
⋂ i ∈ s, ⋂ (j : κ i), f i j = ⋂ ij ∈ Finset.sigma s fun (x : ι) => Finset.univ, f ij.fst ij.snd
instance
Sigma.instFintype
{ι : Type u_1}
{κ : ι → Type u_5}
[(i : ι) → Fintype (κ i)]
[Fintype ι]
:
Fintype ((i : ι) × κ i)
Equations
- Sigma.instFintype = { elems := Finset.sigma Finset.univ fun (x : ι) => Finset.univ, complete := ⋯ }
instance
PSigma.instFintype
{ι : Type u_1}
{κ : ι → Type u_5}
[(i : ι) → Fintype (κ i)]
[Fintype ι]
:
Fintype ((i : ι) ×' κ i)
Equations
- PSigma.instFintype = Fintype.ofEquiv ((i : ι) × κ i) (Equiv.psigmaEquivSigma fun (i : ι) => κ i).symm
@[simp]
theorem
Finset.univ_sigma_univ
{ι : Type u_1}
{κ : ι → Type u_5}
[(i : ι) → Fintype (κ i)]
[Fintype ι]
:
(Finset.sigma Finset.univ fun (x : ι) => Finset.univ) = Finset.univ