feat: Unions and intersections indexed by Finset.sigma (#10851)

Followup to #8964 From PFR
leanprover-community · Feb 28, 2024 · e69cb64 · e69cb64
1 parent f5e8fa1
commit e69cb64
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 12 deletions.
diff --git a/Mathlib/Data/Fintype/Card.lean b/Mathlib/Data/Fintype/Card.lean
@@ -541,6 +541,8 @@ theorem card_eq_zero_iff : card α = 0 ↔ IsEmpty α := by
   card_eq_zero_iff.2 ‹_›
 #align fintype.card_eq_zero Fintype.card_eq_zero
 
+alias card_of_isEmpty := card_eq_zero
+
 theorem card_eq_one_iff_nonempty_unique : card α = 1 ↔ Nonempty (Unique α) :=
   ⟨fun h =>
     let ⟨d, h⟩ := Fintype.card_eq_one_iff.mp h

diff --git a/Mathlib/Data/Fintype/Sigma.lean b/Mathlib/Data/Fintype/Sigma.lean
@@ -19,20 +19,27 @@ open Nat
 
 universe u v
 
-variable {α β γ : Type*}
+variable {ι α β γ : Type*} {κ : ι → Type*} [Π i, Fintype (κ i)]
 
 open Finset Function
 
-instance {α : Type*} (β : α → Type*) [Fintype α] [∀ a, Fintype (β a)] : Fintype (Sigma β) :=
-  ⟨univ.sigma fun _ => univ, fun ⟨a, b⟩ => by simp⟩
+lemma Set.biUnion_finsetSigma_univ (s : Finset ι) (f : Sigma κ → Set α) :
+    ⋃ ij ∈ s.sigma fun _ ↦ Finset.univ, f ij = ⋃ i ∈ s, ⋃ j, f ⟨i, j⟩ := by aesop
 
-@[simp]
-theorem Finset.univ_sigma_univ {α : Type*} {β : α → Type*} [Fintype α] [∀ a, Fintype (β a)] :
-    ((univ : Finset α).sigma fun a => (univ : Finset (β a))) = univ :=
-  rfl
-#align finset.univ_sigma_univ Finset.univ_sigma_univ
+lemma Set.biUnion_finsetSigma_univ' (s : Finset ι) (f : Π i, κ i → Set α) :
+    ⋃ i ∈ s, ⋃ j, f i j = ⋃ ij ∈ s.sigma fun _ ↦ Finset.univ, f ij.1 ij.2 := by aesop
+
+lemma Set.biInter_finsetSigma_univ (s : Finset ι) (f : Sigma κ → Set α) :
+    ⋂ ij ∈ s.sigma fun _ ↦ Finset.univ, f ij = ⋂ i ∈ s, ⋂ j, f ⟨i, j⟩ := by aesop
+
+lemma Set.biInter_finsetSigma_univ' (s : Finset ι) (f : Π i, κ i → Set α) :
+    ⋂ i ∈ s, ⋂ j, f i j = ⋂ ij ∈ s.sigma fun _ ↦ Finset.univ, f ij.1 ij.2 := by aesop
 
-instance PSigma.fintype {α : Type*} {β : α → Type*} [Fintype α] [∀ a, Fintype (β a)] :
-    Fintype (Σ'a, β a) :=
-  Fintype.ofEquiv _ (Equiv.psigmaEquivSigma _).symm
-#align psigma.fintype PSigma.fintype
+variable [Fintype ι] [Π i, Fintype (κ i)]
+
+instance Sigma.instFintype : Fintype (Σ i, κ i) := ⟨univ.sigma fun _ ↦ univ, by simp⟩
+instance PSigma.instFintype : Fintype (Σ' i, κ i) := .ofEquiv _ (Equiv.psigmaEquivSigma _).symm
+#align psigma.fintype PSigma.instFintype
+
+@[simp] lemma Finset.univ_sigma_univ : univ.sigma (fun _ ↦ univ) = (univ : Finset (Σ i, κ i)) := rfl
+#align finset.univ_sigma_univ Finset.univ_sigma_univ