English
Let P be a monotone predicate on sets in the sense that if t extends s and P(t) holds then P(s) holds. Then s is maximal for P if and only if P(s) holds and no element outside s can be added without destroying P.
Русский
Пусть P — свойство над множествами, так что если t содержит s и P(t) выполняется, то P(s) выполняется. Тогда s максимальна по P тогда и только тогда, когда P(s) выполняется и для любого x вне s вставка x в s нарушает P.
LaTeX
$$$\\text{Maximal } P\\, s \\;\\Longleftrightarrow\\; P(s) \\wedge \\forall x \\notin s, \\; \\neg P(\\mathrm{insert}\\ x\\ s).$$$
Lean4
theorem maximal_iff_forall_insert (hP : ∀ ⦃s t⦄, P t → s ⊆ t → P s) : Maximal P s ↔ P s ∧ ∀ x ∉ s, ¬P (insert x s) :=
by
simp only [not_imp_not]
exact
⟨fun h ↦ ⟨h.1, fun x ↦ h.mem_of_prop_insert⟩, fun h ↦
⟨h.1, fun t ht hst x hxt ↦ h.2 x (hP ht <| insert_subset hxt hst)⟩⟩
