English
The size of 𝒜 is at most the size of its shatterer: #𝒜 ≤ #𝒜.shatterer.
Русский
Размер 𝒜 не превосходит размера 𝒜.shatterer: #𝒜 ≤ #𝒜.shatterer.
LaTeX
$$$#\\mathcal{A} \\le #\\mathcal{A}.shatterer$$$
Lean4
/-- Pajor's variant of the **Sauer-Shelah lemma**. -/
theorem card_le_card_shatterer (𝒜 : Finset (Finset α)) : #𝒜 ≤ #𝒜.shatterer :=
by
refine memberFamily_induction_on 𝒜 ?_ ?_ ?_
· simp
· rfl
intro a 𝒜 ih₀ ih₁
set ℬ : Finset (Finset α) := ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer).image (insert a)
have hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer) :=
by
refine card_image_of_injOn <| insert_erase_invOn.2.injOn.mono ?_
simp only [coe_inter, Set.subset_def, Set.mem_inter_iff, mem_coe, Set.mem_setOf_eq, and_imp, mem_shatterer]
exact fun s _ ↦ aux (fun t ht ↦ (mem_filter.1 ht).2)
rw [← card_memberSubfamily_add_card_nonMemberSubfamily a]
refine (Nat.add_le_add ih₁ ih₀).trans ?_
rw [← card_union_add_card_inter, ← hℬ, ← card_union_of_disjoint]
swap
· simp only [ℬ, disjoint_left, mem_union, mem_shatterer, mem_image, not_exists, not_and]
rintro _ (hs | hs) s - rfl
· exact aux (fun t ht ↦ (mem_memberSubfamily.1 ht).2) hs <| mem_insert_self _ _
· exact aux (fun t ht ↦ (mem_nonMemberSubfamily.1 ht).2) hs <| mem_insert_self _ _
refine card_mono <| union_subset (union_subset ?_ <| shatterer_mono <| filter_subset _ _) ?_
· simp only [subset_iff, mem_shatterer]
rintro s hs t ht
obtain ⟨u, hu, rfl⟩ := hs ht
rw [mem_memberSubfamily] at hu
refine ⟨insert a u, hu.1, inter_insert_of_notMem fun ha ↦ ?_⟩
obtain ⟨v, hv, hsv⟩ := hs.exists_inter_eq_singleton ha
rw [mem_memberSubfamily] at hv
rw [← singleton_subset_iff (a := a), ← hsv] at hv
exact hv.2 inter_subset_right
· refine forall_mem_image.2 fun s hs ↦ mem_shatterer.2 fun t ht ↦ ?_
simp only [mem_inter, mem_shatterer] at hs
rw [subset_insert_iff] at ht
by_cases ha : a ∈ t
· obtain ⟨u, hu, hsu⟩ := hs.1 ht
rw [mem_memberSubfamily] at hu
refine ⟨_, hu.1, ?_⟩
rw [← insert_inter_distrib, hsu, insert_erase ha]
· obtain ⟨u, hu, hsu⟩ := hs.2 ht
rw [mem_nonMemberSubfamily] at hu
refine ⟨_, hu.1, ?_⟩
rwa [insert_inter_of_notMem hu.2, hsu, erase_eq_self]
