feat(data/finset/slice): r-sets and slice (#10685)

Two simple nonetheless useful definitions about set families. A family of `r`-sets is a set of finsets of cardinality `r`. The slice of a set family is its subset of `r`-sets.

src/combinatorics/set_family/shadow.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta, Alena Gusakov, Yaël Dillies
 -/
-import data.fintype.basic
+import data.finset.slice
 import logic.function.iterate
 
 /-!
@@ -46,7 +46,7 @@ variables {α : Type*}
 
 namespace finset
 section shadow
-variables [decidable_eq α] {𝒜 : finset (finset α)} {s t : finset α} {a : α} {k : ℕ}
+variables [decidable_eq α] {𝒜 : finset (finset α)} {s t : finset α} {a : α} {k r : ℕ}
 
 /-- The shadow of a set family `𝒜` is all sets we can get by removing one element from any set in
 `𝒜`, and the (`k` times) iterated shadow (`shadow^[k]`) is all sets we can get by removing `k`
@@ -70,6 +70,16 @@ by simp only [shadow, mem_sup, mem_image]
 lemma erase_mem_shadow (hs : s ∈ 𝒜) (ha : a ∈ s) : erase s a ∈ ∂ 𝒜 :=
 mem_shadow_iff.2 ⟨s, hs, a, ha, rfl⟩
 
+/-- The shadow of a family of `r`-sets is a family of `r - 1`-sets. -/
+protected lemma sized.shadow (h𝒜 : (𝒜 : set (finset α)).sized r) :
+  (∂ 𝒜 : set (finset α)).sized (r - 1) :=
+begin
+  intros A h,
+  obtain ⟨A, hA, i, hi, rfl⟩ := mem_shadow_iff.1 h,
+  rw [card_erase_of_mem hi, h𝒜 hA],
+  refl,
+end
+
 /-- `t` is in the shadow of `𝒜` iff we can add an element to it so that the resulting finset is in
 `𝒜`. -/
 lemma mem_shadow_iff_insert_mem : s ∈ ∂ 𝒜 ↔ ∃ a ∉ s, insert a s ∈ 𝒜 :=
@@ -132,21 +142,20 @@ end shadow
 open_locale finset_family
 
 section up_shadow
-variables [decidable_eq α] [fintype α] {𝒜 : finset (finset α)} {s t : finset α} {a : α} {k : ℕ}
+variables [decidable_eq α] [fintype α] {𝒜 : finset (finset α)} {s t : finset α} {a : α} {k r : ℕ}
 
 /-- The upper shadow of a set family `𝒜` is all sets we can get by adding one element to any set in
 `𝒜`, and the (`k` times) iterated upper shadow (`up_shadow^[k]`) is all sets we can get by adding
-`k`
-elements from any set in `𝒜`. -/
+`k` elements from any set in `𝒜`. -/
 def up_shadow (𝒜 : finset (finset α)) : finset (finset α) :=
 𝒜.sup $ λ s, sᶜ.image $ λ a, insert a s
 
 localized "notation `∂⁺ `:90 := finset.up_shadow" in finset_family
 
-/-- The up_shadow of the empty set is empty. -/
+/-- The upper shadow of the empty set is empty. -/
 @[simp] lemma up_shadow_empty : ∂⁺ (∅ : finset (finset α)) = ∅ := rfl
 
-/-- The up_shadow is monotone. -/
+/-- The upper shadow is monotone. -/
 @[mono] lemma up_shadow_monotone : monotone (up_shadow : finset (finset α) → finset (finset α)) :=
 λ 𝒜 ℬ, sup_mono
 
@@ -158,6 +167,15 @@ by simp_rw [up_shadow, mem_sup, mem_image, exists_prop, mem_compl]
 lemma insert_mem_up_shadow (hs : s ∈ 𝒜) (ha : a ∉ s) : insert a s ∈ ∂⁺ 𝒜 :=
 mem_up_shadow_iff.2 ⟨s, hs, a, ha, rfl⟩
 
+/-- The upper shadow of a family of `r`-sets is a family of `r + 1`-sets. -/
+protected lemma sized.up_shadow (h𝒜 : (𝒜 : set (finset α)).sized r) :
+  (∂⁺ 𝒜 : set (finset α)).sized (r + 1) :=
+begin
+  intros A h,
+  obtain ⟨A, hA, i, hi, rfl⟩ := mem_up_shadow_iff.1 h,
+  rw [card_insert_of_not_mem hi, h𝒜 hA],
+end
+
 /-- `t` is in the upper shadow of `𝒜` iff we can remove an element from it so that the resulting
 finset is in `𝒜`. -/
 lemma mem_up_shadow_iff_erase_mem : s ∈ ∂⁺ 𝒜 ↔ ∃ a ∈ s, s.erase a ∈ 𝒜 :=
@@ -184,7 +202,7 @@ begin
     rwa [←sdiff_singleton_eq_erase, ←ha, sdiff_sdiff_eq_self hts] }
 end
 
-/-- Being in the up_shadow of `𝒜` means we have a superset in `𝒜`. -/
+/-- Being in the upper shadow of `𝒜` means we have a superset in `𝒜`. -/
 lemma exists_subset_of_mem_up_shadow (hs : s ∈ ∂⁺ 𝒜) : ∃ t ∈ 𝒜, t ⊆ s :=
 let ⟨t, ht, hts, _⟩ := mem_up_shadow_iff_exists_mem_card_add_one.1 hs in ⟨t, ht, hts⟩
 

src/data/finset/slice.lean

@@ -0,0 +1,103 @@
+/-
+Copyright (c) 2021 Bhavik Mehta, Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bhavik Mehta, Alena Gusakov, Yaël Dillies
+-/
+import data.fintype.basic
+import order.antichain
+
+/-!
+# `r`-sets and slice
+
+This file defines the `r`-th slice of a set family and provides a way to say that a set family is
+made of `r`-sets.
+
+An `r`-set is a finset of cardinality `r` (aka of *size* `r`). The `r`-th slice of a set family is
+the set family made of its `r`-sets.
+
+## Main declarations
+
+* `set.sized`: `A.sized r` means that `A` only contains `r`-sets.
+* `finset.slice`: `A.slice r` is the set of `r`-sets in `A`.
+
+## Notation
+
+`A # r` is notation for `A.slice r` in locale `finset_family`.
+-/
+
+open finset nat
+
+variables {α : Type*}
+
+namespace set
+variables {A B : set (finset α)} {r : ℕ}
+
+/-! ### Families of `r`-sets -/
+
+/-- `sized r A` means that every finset in `A` has size `r`. -/
+def sized (r : ℕ) (A : set (finset α)) : Prop := ∀ ⦃x⦄, x ∈ A → card x = r
+
+lemma sized.mono (h : A ⊆ B) (hB : B.sized r) : A.sized r := λ x hx, hB $ h hx
+
+lemma sized_union : (A ∪ B).sized r ↔ A.sized r ∧ B.sized r :=
+⟨λ hA, ⟨hA.mono $ subset_union_left _ _, hA.mono $ subset_union_right _ _⟩,
+  λ hA x hx, hx.elim (λ h, hA.1 h) $ λ h, hA.2 h⟩
+
+alias sized_union ↔ _ set.sized.union
+
+protected lemma sized.is_antichain (hA : A.sized r) : is_antichain (⊆) A :=
+λ s hs t ht h hst, h $ eq_of_subset_of_card_le hst ((hA ht).trans (hA hs).symm).le
+
+end set
+
+namespace finset
+section sized
+variables [fintype α] {𝒜 : finset (finset α)} {s : finset α} {r : ℕ}
+
+lemma subset_powerset_len_univ_iff : 𝒜 ⊆ powerset_len r univ ↔ (𝒜 : set (finset α)).sized r :=
+forall_congr $ λ A, by rw [mem_powerset_len_univ_iff, mem_coe]
+
+alias subset_powerset_len_univ_iff  ↔ _ set.sized.subset_powerset_len_univ
+
+lemma _root_.set.sized.card_le (h𝒜 : (𝒜 : set (finset α)).sized r) :
+  card 𝒜 ≤ (fintype.card α).choose r :=
+begin
+  rw [fintype.card, ←card_powerset_len],
+  exact card_le_of_subset h𝒜.subset_powerset_len_univ,
+end
+
+end sized
+
+/-! ### Slices -/
+
+section slice
+variables {𝒜 : finset (finset α)} {A A₁ A₂ : finset α} {r r₁ r₂ : ℕ}
+
+/-- The `r`-th slice of a set family is the subset of its elements which have cardinality `r`. -/
+def slice (𝒜 : finset (finset α)) (r : ℕ) : finset (finset α) := 𝒜.filter (λ i, i.card = r)
+
+localized "infix ` # `:90 := finset.slice" in finset_family
+
+/-- `A` is in the `r`-th slice of `𝒜` iff it's in `𝒜` and has cardinality `r`. -/
+lemma mem_slice : A ∈ 𝒜 # r ↔ A ∈ 𝒜 ∧ A.card = r := mem_filter
+
+/-- The `r`-th slice of `𝒜` is a subset of `𝒜`. -/
+lemma slice_subset : 𝒜 # r ⊆ 𝒜 := filter_subset _ _
+
+/-- Everything in the `r`-th slice of `𝒜` has size `r`. -/
+lemma sized_slice : (𝒜 # r : set (finset α)).sized r := λ _, and.right ∘ mem_slice.mp
+
+lemma eq_of_mem_slice (h₁ : A ∈ 𝒜 # r₁) (h₂ : A ∈ 𝒜 # r₂) : r₁ = r₂ :=
+(sized_slice h₁).symm.trans $ sized_slice h₂
+
+/-- Elements in distinct slices must be distinct. -/
+lemma ne_of_mem_slice (h₁ : A₁ ∈ 𝒜 # r₁) (h₂ : A₂ ∈ 𝒜 # r₂) : r₁ ≠ r₂ → A₁ ≠ A₂ :=
+mt $ λ h, (sized_slice h₁).symm.trans ((congr_arg card h).trans (sized_slice h₂))
+
+variables [decidable_eq α]
+
+lemma pairwise_disjoint_slice : (set.univ : set ℕ).pairwise_disjoint (slice 𝒜) :=
+λ m _ n _ hmn, disjoint_filter.2 $ λ s hs hm hn, hmn $ hm.symm.trans hn
+
+end slice
+end finset

src/data/fintype/basic.lean

@@ -1291,6 +1291,10 @@ fintype.of_equiv _ sym.sym_equiv_sym'.symm
   fintype.card (finset α) = 2 ^ (fintype.card α) :=
 finset.card_powerset finset.univ
 
+lemma finset.mem_powerset_len_univ_iff [fintype α] {s : finset α} {k : ℕ} :
+  s ∈ powerset_len k (univ : finset α) ↔ card s = k :=
+mem_powerset_len.trans $ and_iff_right $ subset_univ _
+
 @[simp] lemma finset.univ_filter_card_eq (α : Type*) [fintype α] (k : ℕ) :
   (finset.univ : finset (finset α)).filter (λ s, s.card = k) = finset.univ.powerset_len k :=
 by { ext, simp [finset.mem_powerset_len] }