English
For a maximal intersecting family s, the maximum is achieved exactly when 2|s| = |α|.
Русский
Для максимального пересекающегося семейства s максимум достигается тогда, когда 2|s| = |α|.
LaTeX
$$$\big(\forall t, (t \text{ Intersecting} \Rightarrow s \subseteq t \Rightarrow s=t)\big) \iff 2 \cdot |s| = |\alpha|$$$
Lean4
theorem is_max_iff_card_eq (hs : (s : Set α).Intersecting) :
(∀ t : Finset α, (t : Set α).Intersecting → s ⊆ t → s = t) ↔ 2 * #s = Fintype.card α := by
classical
refine
⟨fun h ↦ ?_, fun h t ht hst ↦
Finset.eq_of_subset_of_card_le hst <| Nat.le_of_mul_le_mul_left (ht.card_le.trans_eq h.symm) Nat.two_pos⟩
suffices s.disjUnion (s.map ⟨compl, compl_injective⟩) hs.disjoint_map_compl = Finset.univ by
rw [Fintype.card, ← this, Nat.two_mul, card_disjUnion, card_map]
rw [← coe_eq_univ, disjUnion_eq_union, coe_union, coe_map, Function.Embedding.coeFn_mk,
image_eq_preimage_of_inverse compl_compl compl_compl]
refine eq_univ_of_forall fun a => ?_
simp_rw [mem_union, mem_preimage]
by_contra! ha
refine s.ne_insert_of_notMem _ ha.1 (h _ ?_ <| s.subset_insert _)
rw [coe_insert]
refine hs.insert ?_ fun b hb hab => ha.2 <| (hs.isUpperSet' h) hab.le_compl_left hb
rintro rfl
have := h {⊤} (by rw [coe_singleton]; exact intersecting_singleton.2 top_ne_bot)
rw [compl_bot] at ha
rw [coe_eq_empty.1 ((hs.isUpperSet' h).top_notMem.1 ha.2)] at this
exact Finset.singleton_ne_empty _ (this <| Finset.empty_subset _).symm
