English
Let P be a property on a partially ordered set (α, ≤) and x ∈ α. Then x is a maximal element satisfying P if and only if P(x) holds and whenever P(y) holds for some y with x ≤ y, we must have x = y. Equivalently, there is no y ≠ x with P(y) and x ≤ y.
Русский
Пусть P — свойство на частично упорядоченном множестве (α, ≤) и x ∈ α. Тогда x является максимальным элементом, удовлетворяющим P, если P(x) выполняется и для любого y с P(y) выполняется: если x ≤ y, то x = y. Эквивалентно: не существует y ≠ x с P(y) и x ≤ y.
LaTeX
$$$$\\text{Maximal } P x \\Longleftrightarrow P x \\land \\forall y\\,(P y \\to x \\le y \\to x = y).$$$$
Lean4
theorem maximal_iff : Maximal P x ↔ P x ∧ ∀ ⦃y⦄, P y → x ≤ y → x = y :=
minimal_iff (α := αᵒᵈ)
