English
A finite-sets version of the maximal intersecting implies upper set principle: if s is a finite set of finite sets and is intersecting, then it satisfies the corresponding upper-set property.
Русский
Для конечного случая вывод аналогичного свойства верхнего множества: если s содержит конечные множества и является пересекающим, выполняется соответствующее верхнее свойство.
LaTeX
$$$\forall s:\, \text{Finset}(\text{Finset}(\alpha)),\; s.\text{Intersecting} \Rightarrow \Big( \forall t, t.\text{Intersecting} \land s \subseteq t \Rightarrow s=t \Big) \Rightarrow \text{IsUpperSet}(s)$$$
Lean4
/-- Maximal intersecting families are upper sets. Finset version. -/
theorem isUpperSet' {s : Finset α} (hs : (s : Set α).Intersecting)
(h : ∀ t : Finset α, (t : Set α).Intersecting → s ⊆ t → s = t) : IsUpperSet (s : Set α) := by
classical
rintro a b hab ha
rw [h (Insert.insert b s) _ (Finset.subset_insert _ _)]
· exact mem_insert_self _ _
rw [coe_insert]
exact hs.insert (mt (eq_bot_mono hab) <| hs.ne_bot ha) fun c hc hbc => hs ha hc <| hbc.mono_left hab
