chore: rename Finset.powersetLen to powersetCard (#7667)

I don't understand why this was ever named `powersetLen`, there isn't even the notion of the length of a Finset/Multiset.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib/Algebra/BigOperators/Basic.lean

@@ -1460,12 +1460,12 @@ theorem prod_pow (s : Finset α) (n : ℕ) (f : α → β) : ∏ x in s, f x ^ n
 #align finset.prod_pow Finset.prod_pow
 #align finset.sum_nsmul Finset.sum_nsmul
 
-/-- A product over `Finset.powersetLen` which only depends on the size of the sets is constant. -/
+/-- A product over `Finset.powersetCard` which only depends on the size of the sets is constant. -/
 @[to_additive
-"A sum over `Finset.powersetLen` which only depends on the size of the sets is constant."]
-lemma prod_powersetLen (n : ℕ) (s : Finset α) (f : ℕ → β) :
-    ∏ t in powersetLen n s, f t.card = f n ^ s.card.choose n := by
-  rw [prod_eq_pow_card, card_powersetLen]; rintro a ha; rw [(mem_powersetLen.1 ha).2]
+"A sum over `Finset.powersetCard` which only depends on the size of the sets is constant."]
+lemma prod_powersetCard (n : ℕ) (s : Finset α) (f : ℕ → β) :
+    ∏ t in powersetCard n s, f t.card = f n ^ s.card.choose n := by
+  rw [prod_eq_pow_card, card_powersetCard]; rintro a ha; rw [(mem_powersetCard.1 ha).2]
 
 @[to_additive]
 theorem prod_flip {n : ℕ} (f : ℕ → β) :
@@ -2133,11 +2133,11 @@ theorem finset_sum_eq_sup_iff_disjoint {β : Type*} {i : Finset β} {f : β →
 #align multiset.finset_sum_eq_sup_iff_disjoint Multiset.finset_sum_eq_sup_iff_disjoint
 
 theorem sup_powerset_len {α : Type*} [DecidableEq α] (x : Multiset α) :
-    (Finset.sup (Finset.range (card x + 1)) fun k => x.powersetLen k) = x.powerset := by
+    (Finset.sup (Finset.range (card x + 1)) fun k => x.powersetCard k) = x.powerset := by
   convert bind_powerset_len x using 1
   rw [Multiset.bind, Multiset.join, ← Finset.range_val, ← Finset.sum_eq_multiset_sum]
   exact
-    Eq.symm (finset_sum_eq_sup_iff_disjoint.mpr fun _ _ _ _ h => pairwise_disjoint_powersetLen x h)
+    Eq.symm (finset_sum_eq_sup_iff_disjoint.mpr fun _ _ _ _ h => pairwise_disjoint_powersetCard x h)
 #align multiset.sup_powerset_len Multiset.sup_powerset_len
 
 @[simp]

Mathlib/Algebra/BigOperators/Ring.lean

@@ -263,7 +263,7 @@ theorem prod_powerset_insert [DecidableEq α] [CommMonoid β] {s : Finset α} {x
       "A sum over `powerset s` is equal to the double sum over sets of subsets of `s` with
       `card s = k`, for `k = 1, ..., card s`"]
 theorem prod_powerset [CommMonoid β] (s : Finset α) (f : Finset α → β) :
-    ∏ t in powerset s, f t = ∏ j in range (card s + 1), ∏ t in powersetLen j s, f t := by
+    ∏ t in powerset s, f t = ∏ j in range (card s + 1), ∏ t in powersetCard j s, f t := by
   rw [powerset_card_disjiUnion, prod_disjiUnion]
 #align finset.prod_powerset Finset.prod_powerset
 #align finset.sum_powerset Finset.sum_powerset

Mathlib/Combinatorics/Additive/SalemSpencer.lean

@@ -402,13 +402,13 @@ theorem le_mulRothNumber_product (s : Finset α) (t : Finset β) :
 
 @[to_additive]
 theorem mulRothNumber_lt_of_forall_not_mulSalemSpencer
-    (h : ∀ t ∈ powersetLen n s, ¬MulSalemSpencer ((t : Finset α) : Set α)) :
+    (h : ∀ t ∈ powersetCard n s, ¬MulSalemSpencer ((t : Finset α) : Set α)) :
     mulRothNumber s < n := by
   obtain ⟨t, hts, hcard, ht⟩ := mulRothNumber_spec s
   rw [← hcard, ← not_le]
   intro hn
   obtain ⟨u, hut, rfl⟩ := exists_smaller_set t n hn
-  exact h _ (mem_powersetLen.2 ⟨hut.trans hts, rfl⟩) (ht.mono hut)
+  exact h _ (mem_powersetCard.2 ⟨hut.trans hts, rfl⟩) (ht.mono hut)
 #align mul_roth_number_lt_of_forall_not_mul_salem_spencer mulRothNumber_lt_of_forall_not_mulSalemSpencer
 #align add_roth_number_lt_of_forall_not_add_salem_spencer addRothNumber_lt_of_forall_not_addSalemSpencer
 

Mathlib/Combinatorics/SetFamily/LYM.lean

@@ -123,13 +123,13 @@ variable [DecidableEq α] (k : ℕ) (𝒜 : Finset (Finset α))
 
 /-- `falling k 𝒜` is all the finsets of cardinality `k` which are a subset of something in `𝒜`. -/
 def falling : Finset (Finset α) :=
-  𝒜.sup <| powersetLen k
+  𝒜.sup <| powersetCard k
 #align finset.falling Finset.falling
 
 variable {𝒜 k} {s : Finset α}
 
 theorem mem_falling : s ∈ falling k 𝒜 ↔ (∃ t ∈ 𝒜, s ⊆ t) ∧ s.card = k := by
-  simp_rw [falling, mem_sup, mem_powersetLen]
+  simp_rw [falling, mem_sup, mem_powersetCard]
   aesop
 #align finset.mem_falling Finset.mem_falling
 

Mathlib/Data/Finset/Powerset.lean

@@ -190,148 +190,150 @@ def decidableForallOfDecidableSSubsets' {s : Finset α} {p : Finset α → Prop}
 
 end SSubsets
 
-section PowersetLen
+section powersetCard
 
-/-- Given an integer `n` and a finset `s`, then `powersetLen n s` is the finset of subsets of `s`
+/-- Given an integer `n` and a finset `s`, then `powersetCard n s` is the finset of subsets of `s`
 of cardinality `n`. -/
-def powersetLen (n : ℕ) (s : Finset α) : Finset (Finset α) :=
-  ⟨((s.1.powersetLen n).pmap Finset.mk) fun _t h => nodup_of_le (mem_powersetLen.1 h).1 s.2,
-    s.2.powersetLen.pmap fun _a _ha _b _hb => congr_arg Finset.val⟩
-#align finset.powerset_len Finset.powersetLen
+def powersetCard (n : ℕ) (s : Finset α) : Finset (Finset α) :=
+  ⟨((s.1.powersetCard n).pmap Finset.mk) fun _t h => nodup_of_le (mem_powersetCard.1 h).1 s.2,
+    s.2.powersetCard.pmap fun _a _ha _b _hb => congr_arg Finset.val⟩
+#align finset.powerset_len Finset.powersetCard
 
 /-- **Formula for the Number of Combinations** -/
-theorem mem_powersetLen {n} {s t : Finset α} : s ∈ powersetLen n t ↔ s ⊆ t ∧ card s = n := by
-  cases s; simp [powersetLen, val_le_iff.symm]
-#align finset.mem_powerset_len Finset.mem_powersetLen
+theorem mem_powersetCard {n} {s t : Finset α} : s ∈ powersetCard n t ↔ s ⊆ t ∧ card s = n := by
+  cases s; simp [powersetCard, val_le_iff.symm]
+#align finset.mem_powerset_len Finset.mem_powersetCard
 
 @[simp]
-theorem powersetLen_mono {n} {s t : Finset α} (h : s ⊆ t) : powersetLen n s ⊆ powersetLen n t :=
-  fun _u h' => mem_powersetLen.2 <| And.imp (fun h₂ => Subset.trans h₂ h) id (mem_powersetLen.1 h')
-#align finset.powerset_len_mono Finset.powersetLen_mono
+theorem powersetCard_mono {n} {s t : Finset α} (h : s ⊆ t) : powersetCard n s ⊆ powersetCard n t :=
+  fun _u h' => mem_powersetCard.2 <|
+    And.imp (fun h₂ => Subset.trans h₂ h) id (mem_powersetCard.1 h')
+#align finset.powerset_len_mono Finset.powersetCard_mono
 
 /-- **Formula for the Number of Combinations** -/
 @[simp]
-theorem card_powersetLen (n : ℕ) (s : Finset α) : card (powersetLen n s) = Nat.choose (card s) n :=
-  (card_pmap _ _ _).trans (Multiset.card_powersetLen n s.1)
-#align finset.card_powerset_len Finset.card_powersetLen
+theorem card_powersetCard (n : ℕ) (s : Finset α) :
+    card (powersetCard n s) = Nat.choose (card s) n :=
+  (card_pmap _ _ _).trans (Multiset.card_powersetCard n s.1)
+#align finset.card_powerset_len Finset.card_powersetCard
 
 @[simp]
-theorem powersetLen_zero (s : Finset α) : Finset.powersetLen 0 s = {∅} := by
-  ext; rw [mem_powersetLen, mem_singleton, card_eq_zero]
+theorem powersetCard_zero (s : Finset α) : Finset.powersetCard 0 s = {∅} := by
+  ext; rw [mem_powersetCard, mem_singleton, card_eq_zero]
   refine'
     ⟨fun h => h.2, fun h => by
       rw [h]
       exact ⟨empty_subset s, rfl⟩⟩
-#align finset.powerset_len_zero Finset.powersetLen_zero
+#align finset.powerset_len_zero Finset.powersetCard_zero
 
 @[simp]
-theorem powersetLen_empty (n : ℕ) {s : Finset α} (h : s.card < n) : powersetLen n s = ∅ :=
-  Finset.card_eq_zero.mp (by rw [card_powersetLen, Nat.choose_eq_zero_of_lt h])
-#align finset.powerset_len_empty Finset.powersetLen_empty
+theorem powersetCard_empty (n : ℕ) {s : Finset α} (h : s.card < n) : powersetCard n s = ∅ :=
+  Finset.card_eq_zero.mp (by rw [card_powersetCard, Nat.choose_eq_zero_of_lt h])
+#align finset.powerset_len_empty Finset.powersetCard_empty
 
-theorem powersetLen_eq_filter {n} {s : Finset α} :
-    powersetLen n s = (powerset s).filter fun x => x.card = n := by
+theorem powersetCard_eq_filter {n} {s : Finset α} :
+    powersetCard n s = (powerset s).filter fun x => x.card = n := by
   ext
-  simp [mem_powersetLen]
-#align finset.powerset_len_eq_filter Finset.powersetLen_eq_filter
+  simp [mem_powersetCard]
+#align finset.powerset_len_eq_filter Finset.powersetCard_eq_filter
 
-theorem powersetLen_succ_insert [DecidableEq α] {x : α} {s : Finset α} (h : x ∉ s) (n : ℕ) :
-    powersetLen n.succ (insert x s) =
-    powersetLen n.succ s ∪ (powersetLen n s).image (insert x) := by
-  rw [powersetLen_eq_filter, powerset_insert, filter_union, ← powersetLen_eq_filter]
+theorem powersetCard_succ_insert [DecidableEq α] {x : α} {s : Finset α} (h : x ∉ s) (n : ℕ) :
+    powersetCard n.succ (insert x s) =
+    powersetCard n.succ s ∪ (powersetCard n s).image (insert x) := by
+  rw [powersetCard_eq_filter, powerset_insert, filter_union, ← powersetCard_eq_filter]
   congr
-  rw [powersetLen_eq_filter, image_filter]
+  rw [powersetCard_eq_filter, image_filter]
   congr 1
   ext t
   simp only [mem_powerset, mem_filter, Function.comp_apply, and_congr_right_iff]
   intro ht
   have : x ∉ t := fun H => h (ht H)
   simp [card_insert_of_not_mem this, Nat.succ_inj']
-#align finset.powerset_len_succ_insert Finset.powersetLen_succ_insert
+#align finset.powerset_len_succ_insert Finset.powersetCard_succ_insert
 
-theorem powersetLen_nonempty {n : ℕ} {s : Finset α} (h : n ≤ s.card) :
-    (powersetLen n s).Nonempty := by
+theorem powersetCard_nonempty {n : ℕ} {s : Finset α} (h : n ≤ s.card) :
+    (powersetCard n s).Nonempty := by
   classical
     induction' s using Finset.induction_on with x s hx IH generalizing n
     · rw [card_empty, le_zero_iff] at h
-      rw [h, powersetLen_zero]
+      rw [h, powersetCard_zero]
       exact Finset.singleton_nonempty _
     · cases n
       · simp
       · rw [card_insert_of_not_mem hx, Nat.succ_le_succ_iff] at h
-        rw [powersetLen_succ_insert hx]
+        rw [powersetCard_succ_insert hx]
         refine' Nonempty.mono _ ((IH h).image (insert x))
         exact subset_union_right _ _
-#align finset.powerset_len_nonempty Finset.powersetLen_nonempty
+#align finset.powerset_len_nonempty Finset.powersetCard_nonempty
 
 @[simp]
-theorem powersetLen_self (s : Finset α) : powersetLen s.card s = {s} := by
+theorem powersetCard_self (s : Finset α) : powersetCard s.card s = {s} := by
   ext
-  rw [mem_powersetLen, mem_singleton]
+  rw [mem_powersetCard, mem_singleton]
   constructor
   · exact fun ⟨hs, hc⟩ => eq_of_subset_of_card_le hs hc.ge
   · rintro rfl
     simp
-#align finset.powerset_len_self Finset.powersetLen_self
+#align finset.powerset_len_self Finset.powersetCard_self
 
-theorem pairwise_disjoint_powersetLen (s : Finset α) :
-    Pairwise fun i j => Disjoint (s.powersetLen i) (s.powersetLen j) := fun _i _j hij =>
+theorem pairwise_disjoint_powersetCard (s : Finset α) :
+    Pairwise fun i j => Disjoint (s.powersetCard i) (s.powersetCard j) := fun _i _j hij =>
   Finset.disjoint_left.mpr fun _x hi hj =>
-    hij <| (mem_powersetLen.mp hi).2.symm.trans (mem_powersetLen.mp hj).2
-#align finset.pairwise_disjoint_powerset_len Finset.pairwise_disjoint_powersetLen
+    hij <| (mem_powersetCard.mp hi).2.symm.trans (mem_powersetCard.mp hj).2
+#align finset.pairwise_disjoint_powerset_len Finset.pairwise_disjoint_powersetCard
 
 theorem powerset_card_disjiUnion (s : Finset α) :
     Finset.powerset s =
-      (range (s.card + 1)).disjiUnion (fun i => powersetLen i s)
-        (s.pairwise_disjoint_powersetLen.set_pairwise _) := by
+      (range (s.card + 1)).disjiUnion (fun i => powersetCard i s)
+        (s.pairwise_disjoint_powersetCard.set_pairwise _) := by
   refine' ext fun a => ⟨fun ha => _, fun ha => _⟩
   · rw [mem_disjiUnion]
     exact
       ⟨a.card, mem_range.mpr (Nat.lt_succ_of_le (card_le_of_subset (mem_powerset.mp ha))),
-        mem_powersetLen.mpr ⟨mem_powerset.mp ha, rfl⟩⟩
+        mem_powersetCard.mpr ⟨mem_powerset.mp ha, rfl⟩⟩
   · rcases mem_disjiUnion.mp ha with ⟨i, _hi, ha⟩
-    exact mem_powerset.mpr (mem_powersetLen.mp ha).1
+    exact mem_powerset.mpr (mem_powersetCard.mp ha).1
 #align finset.powerset_card_disj_Union Finset.powerset_card_disjiUnion
 
 theorem powerset_card_biUnion [DecidableEq (Finset α)] (s : Finset α) :
-    Finset.powerset s = (range (s.card + 1)).biUnion fun i => powersetLen i s := by
+    Finset.powerset s = (range (s.card + 1)).biUnion fun i => powersetCard i s := by
   simpa only [disjiUnion_eq_biUnion] using powerset_card_disjiUnion s
 #align finset.powerset_card_bUnion Finset.powerset_card_biUnion
 
-theorem powersetLen_sup [DecidableEq α] (u : Finset α) (n : ℕ) (hn : n < u.card) :
-    (powersetLen n.succ u).sup id = u := by
+theorem powersetCard_sup [DecidableEq α] (u : Finset α) (n : ℕ) (hn : n < u.card) :
+    (powersetCard n.succ u).sup id = u := by
   apply le_antisymm
-  · simp_rw [Finset.sup_le_iff, mem_powersetLen]
+  · simp_rw [Finset.sup_le_iff, mem_powersetCard]
     rintro x ⟨h, -⟩
     exact h
   · rw [sup_eq_biUnion, le_iff_subset, subset_iff]
     cases' (Nat.succ_le_of_lt hn).eq_or_lt with h' h'
     · simp [h']
     · intro x hx
       simp only [mem_biUnion, exists_prop, id.def]
-      obtain ⟨t, ht⟩ : ∃ t, t ∈ powersetLen n (u.erase x) := powersetLen_nonempty
+      obtain ⟨t, ht⟩ : ∃ t, t ∈ powersetCard n (u.erase x) := powersetCard_nonempty
         (le_trans (Nat.le_pred_of_lt hn) pred_card_le_card_erase)
       · refine' ⟨insert x t, _, mem_insert_self _ _⟩
-        rw [← insert_erase hx, powersetLen_succ_insert (not_mem_erase _ _)]
+        rw [← insert_erase hx, powersetCard_succ_insert (not_mem_erase _ _)]
         exact mem_union_right _ (mem_image_of_mem _ ht)
-#align finset.powerset_len_sup Finset.powersetLen_sup
+#align finset.powerset_len_sup Finset.powersetCard_sup
 
 @[simp]
-theorem powersetLen_card_add (s : Finset α) {i : ℕ} (hi : 0 < i) :
-    s.powersetLen (s.card + i) = ∅ :=
-  Finset.powersetLen_empty _ (lt_add_of_pos_right (Finset.card s) hi)
-#align finset.powerset_len_card_add Finset.powersetLen_card_add
+theorem powersetCard_card_add (s : Finset α) {i : ℕ} (hi : 0 < i) :
+    s.powersetCard (s.card + i) = ∅ :=
+  Finset.powersetCard_empty _ (lt_add_of_pos_right (Finset.card s) hi)
+#align finset.powerset_len_card_add Finset.powersetCard_card_add
 
 @[simp]
-theorem map_val_val_powersetLen (s : Finset α) (i : ℕ) :
-    (s.powersetLen i).val.map Finset.val = s.1.powersetLen i := by
-  simp [Finset.powersetLen, map_pmap, pmap_eq_map, map_id']
-#align finset.map_val_val_powerset_len Finset.map_val_val_powersetLen
+theorem map_val_val_powersetCard (s : Finset α) (i : ℕ) :
+    (s.powersetCard i).val.map Finset.val = s.1.powersetCard i := by
+  simp [Finset.powersetCard, map_pmap, pmap_eq_map, map_id']
+#align finset.map_val_val_powerset_len Finset.map_val_val_powersetCard
 
-theorem powersetLen_map {β : Type*} (f : α ↪ β) (n : ℕ) (s : Finset α) :
-    powersetLen n (s.map f) = (powersetLen n s).map (mapEmbedding f).toEmbedding :=
+theorem powersetCard_map {β : Type*} (f : α ↪ β) (n : ℕ) (s : Finset α) :
+    powersetCard n (s.map f) = (powersetCard n s).map (mapEmbedding f).toEmbedding :=
   ext <| fun t => by
-    simp only [card_map, mem_powersetLen, le_eq_subset, gt_iff_lt, mem_map, mapEmbedding_apply]
+    simp only [card_map, mem_powersetCard, le_eq_subset, gt_iff_lt, mem_map, mapEmbedding_apply]
     constructor
     · classical
       intro h
@@ -347,8 +349,8 @@ theorem powersetLen_map {β : Type*} (f : α ↪ β) (n : ℕ) (s : Finset α) :
       --Porting note: Why is `rw` required here and not `simp`?
       rw [mapEmbedding_apply]
       simp [has]
-#align finset.powerset_len_map Finset.powersetLen_map
+#align finset.powerset_len_map Finset.powersetCard_map
 
-end PowersetLen
+end powersetCard
 
 end Finset

Mathlib/Data/Finset/Slice.lean

@@ -94,9 +94,9 @@ theorem Sized.univ_mem_iff [Fintype α] (hA : A.Sized r) : Finset.univ ∈ A ↔
   hA.isAntichain.top_mem_iff
 #align set.sized.univ_mem_iff Set.Sized.univ_mem_iff
 
-theorem sized_powersetLen (s : Finset α) (r : ℕ) : (powersetLen r s : Set (Finset α)).Sized r :=
-  fun _t ht => (mem_powersetLen.1 ht).2
-#align set.sized_powerset_len Set.sized_powersetLen
+theorem sized_powersetCard (s : Finset α) (r : ℕ) : (powersetCard r s : Set (Finset α)).Sized r :=
+  fun _t ht => (mem_powersetCard.1 ht).2
+#align set.sized_powerset_len Set.sized_powersetCard
 
 end Set
 
@@ -106,17 +106,17 @@ section Sized
 
 variable [Fintype α] {𝒜 : Finset (Finset α)} {s : Finset α} {r : ℕ}
 
-theorem subset_powersetLen_univ_iff : 𝒜 ⊆ powersetLen r univ ↔ (𝒜 : Set (Finset α)).Sized r :=
-  forall_congr' fun A => by rw [mem_powersetLen_univ, mem_coe]
-#align finset.subset_powerset_len_univ_iff Finset.subset_powersetLen_univ_iff
+theorem subset_powersetCard_univ_iff : 𝒜 ⊆ powersetCard r univ ↔ (𝒜 : Set (Finset α)).Sized r :=
+  forall_congr' fun A => by rw [mem_powersetCard_univ, mem_coe]
+#align finset.subset_powerset_len_univ_iff Finset.subset_powersetCard_univ_iff
 
-alias ⟨_, _root_.Set.Sized.subset_powersetLen_univ⟩ := subset_powersetLen_univ_iff
-#align set.sized.subset_powerset_len_univ Set.Sized.subset_powersetLen_univ
+alias ⟨_, _root_.Set.Sized.subset_powersetCard_univ⟩ := subset_powersetCard_univ_iff
+#align set.sized.subset_powerset_len_univ Set.Sized.subset_powersetCard_univ
 
 theorem _root_.Set.Sized.card_le (h𝒜 : (𝒜 : Set (Finset α)).Sized r) :
     card 𝒜 ≤ (Fintype.card α).choose r := by
-  rw [Fintype.card, ← card_powersetLen]
-  exact card_le_of_subset (subset_powersetLen_univ_iff.mpr h𝒜)
+  rw [Fintype.card, ← card_powersetCard]
+  exact card_le_of_subset (subset_powersetCard_univ_iff.mpr h𝒜)
 #align set.sized.card_le Set.Sized.card_le
 
 end Sized

Mathlib/Data/Fintype/Powerset.lean

@@ -40,14 +40,14 @@ lemma filter_subset_univ [DecidableEq α] (s : Finset α) :
   rw [← Finset.powerset_univ, powerset_inj]
 #align finset.powerset_eq_univ Finset.powerset_eq_univ
 
-@[simp] lemma mem_powersetLen_univ : s ∈ powersetLen k (univ : Finset α) ↔ card s = k :=
-  mem_powersetLen.trans <| and_iff_right <| subset_univ _
-#align finset.mem_powerset_len_univ_iff Finset.mem_powersetLen_univ
+@[simp] lemma mem_powersetCard_univ : s ∈ powersetCard k (univ : Finset α) ↔ card s = k :=
+  mem_powersetCard.trans <| and_iff_right <| subset_univ _
+#align finset.mem_powerset_len_univ_iff Finset.mem_powersetCard_univ
 
 variable (α)
 
 @[simp] lemma univ_filter_card_eq (k : ℕ) :
-    (univ : Finset (Finset α)).filter (fun s ↦ s.card = k) = univ.powersetLen k := by ext; simp
+    (univ : Finset (Finset α)).filter (fun s ↦ s.card = k) = univ.powersetCard k := by ext; simp
 #align finset.univ_filter_card_eq Finset.univ_filter_card_eq
 
 end Finset