English
A predicate P on subsets has the maximal subset property with respect to X if every I ⊆ X with P I is contained in some J ⊆ X maximal with respect to P.
Русский
predicat P на подмножества имеет свойство существования максимального подмножества относительно X, если каждый I ⊆ X с P I содержится в некотором J ⊆ X, максимальном по свойству P.
LaTeX
$$$$ \ExistsMaximalSubsetProperty \; P \; X \iff \forall I, P I \to I \subseteq X \to \exists J, I \subseteq J \wedge \text{Maximal}(\lambda K \mapsto P K \wedge K \subseteq X) J $$$$
Lean4
/-- A set `X` has the maximal subset property for a predicate `P` if every subset of `X` satisfying
`P` is contained in a maximal subset of `X` satisfying `P`. -/
def ExistsMaximalSubsetProperty {α : Type*} (P : Set α → Prop) (X : Set α) : Prop :=
∀ I, P I → I ⊆ X → ∃ J, I ⊆ J ∧ Maximal (fun K ↦ P K ∧ K ⊆ X) J
