English
If a predicate P on sets satisfies a natural monotonicity condition, and s satisfies P but is not maximal with respect to P, then there exists an element outside s whose insertion into s yields a set still satisfying P.
Русский
Если P удовлетворяет естественному монотонному условию, и множество s удовлетворяет P, но не является максимальным по P, тогда существует элемент вне s, который при вставке в s дает множество, удовлетворяющее P.
LaTeX
$$$\\forall hP,\\; P(s) \\land \\lnot (\\text{Maximal } P\\, s) \\rightarrow \\exists x \\notin s,\\; P(\\mathrm{insert}\\ x\\ s).$$$
Lean4
theorem exists_insert_of_not_maximal (hP : ∀ ⦃s t⦄, P t → s ⊆ t → P s) (hs : P s) (h : ¬Maximal P s) :
∃ x ∉ s, P (insert x s) := by simpa [Set.maximal_iff_forall_insert hP, hs] using h
