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
@[implicit_reducible]
@[implicit_reducible]