English
There exists a larger set t containing s such that 2|t| equals the universe size and t is itself intersecting.
Русский
Существует большее множество t, содержащее s, такое что 2|t| равно размеру универсума и t также пересекающее.
LaTeX
$$$\exists t \; (s \subseteq t) \land (2 \cdot |t| = |\α|) \land (t \text{ Intersecting})$$$
Lean4
theorem exists_card_eq (hs : (s : Set α).Intersecting) :
∃ t, s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (t : Set α).Intersecting :=
by
have := hs.card_le
rw [Nat.mul_comm, ← Nat.le_div_iff_mul_le Nat.two_pos] at this
revert hs
refine s.strongDownwardInductionOn ?_ this
rintro s ih _hcard hs
by_cases h : ∀ t : Finset α, (t : Set α).Intersecting → s ⊆ t → s = t
· exact ⟨s, Subset.rfl, hs.is_max_iff_card_eq.1 h, hs⟩
push_neg at h
obtain ⟨t, ht, hst⟩ := h
refine (ih ?_ (_root_.ssubset_iff_subset_ne.2 hst) ht).imp fun u => And.imp_left hst.1.trans
rw [Nat.le_div_iff_mul_le Nat.two_pos, Nat.mul_comm]
exact ht.card_le
