English
A maximal intersecting family has a dual description via the card equality 2|s| = |α|.
Русский
Максимальное пересекающееся семейство описывается через равенство кардиналностей 2|s| = |α|.
LaTeX
$$$(\forall t, (t \text{ Intersecting}) \Rightarrow s \subseteq t \Rightarrow s=t) \iff 2|s| = |\alpha|$$$
Lean4
/-- Applying the compression makes the set smaller in colex. This is intuitive since a portion of
the set is being "shifted down" as `max U < max V`. -/
theorem toColex_compress_lt_toColex {hU : U.Nonempty} {hV : V.Nonempty} (h : max' U hU < max' V hV)
(hA : compress U V s ≠ s) : toColex (compress U V s) < toColex s :=
by
rw [compress, ite_ne_right_iff] at hA
rw [compress, if_pos hA.1, lt_iff_exists_filter_lt]
simp_rw [mem_sdiff (s := s), filter_inj, and_assoc]
refine ⟨_, hA.1.2 <| max'_mem _ hV, notMem_sdiff_of_mem_right <| max'_mem _ _, fun a ha ↦ ?_⟩
have : a ∉ V := fun H ↦ ha.not_ge (le_max' _ _ H)
have : a ∉ U := fun H ↦ ha.not_gt ((le_max' _ _ H).trans_lt h)
simp [‹a ∉ U›, ‹a ∉ V›]
