English
If a family s of sets is maximal with respect to the intersecting property (i.e., no proper superset is still intersecting), then s is an upper set with respect to inclusion: whenever A ∈ s and A ⊆ B, we have B ∈ s.
Русский
Если семейство множеств является максимальным по отношению к свойству пересечения, то оно является верхним по включению: если A ∈ s и A ⊆ B, тогда B ∈ s.
LaTeX
$$$\text{IsUpperSet}(s) \quad\text{given}\quad (\forall t, t \text{ intersecting } \Rightarrow s \subseteq t \Rightarrow s=t)$$$
Lean4
/-- Maximal intersecting families are upper sets. -/
protected theorem isUpperSet (hs : s.Intersecting) (h : ∀ t : Set α, t.Intersecting → s ⊆ t → s = t) : IsUpperSet s :=
by
classical
rintro a b hab ha
rw [h (Insert.insert b s) _ (subset_insert _ _)]
· exact mem_insert _ _
exact hs.insert (mt (eq_bot_mono hab) <| hs.ne_bot ha) fun c hc hbc => hs ha hc <| hbc.mono_left hab
