English
Let s be a subset of α. An element x ∈ α is a maximal element of s (with respect to ≤) if and only if x ∈ s and every y ∈ s with x ≤ y satisfies y = x. Equivalently, there is no y ∈ s with x < y.
Русский
Пусть s ⊆ α. Элемент x ∈ α является максимальным элементом множества s (относительно ≤) тогда и только тогда, когда x ∈ s и для любого y ∈ s, если x ≤ y, то y = x. Эквивалентно, нет такого y ∈ s, чтобы x < y.
LaTeX
$$$$\\text{Maximal}(\\cdot \\in s)\, x \\Longleftrightarrow x \\in s \\land \\forall y\\,(y \\in s \\to x \\le y \\to x = y). $$$$
Lean4
theorem maximal_mem_iff {s : Set α} : Maximal (· ∈ s) x ↔ x ∈ s ∧ ∀ ⦃y⦄, y ∈ s → x ≤ y → x = y :=
maximal_iff
