English
Let Finset α be equipped with a predicate P: Finset α → Prop which is downward closed under taking subsets (i.e., if P(t) holds and s ⊆ t then P(s) holds). Then Maximal P s holds iff P(s) and for every x ∉ s, P(insert x s) is false.
Русский
Пусть P: Finset α → Prop является нисходяще замкнутой по включению. Тогда максимальность P по s эквивалентна: P(s) и для любого x не в s, P(insert x s) ложно.
LaTeX
$$$$\\text{Maximal } P(s) \\iff P(s) \\land \\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 [Maximal, and_congr_right_iff]
exact fun _ ↦
⟨fun h x hxs hx ↦ hxs <| h hx (subset_insert _ _) (mem_insert_self x s), fun h t ht hst x hxt ↦
by_contra fun hxs ↦ h x hxs (hP ht (insert_subset hxt hst))⟩
