maximal_iff_forall_gt — Mathlib

English

In a preorder, maximal P x is equivalent to P x together with the property that no y greater than x satisfies P y.

Русский

В порядке образует максимальность P у x как P x плюс свойство, что не существует y > x с P y.

LaTeX

$$$ \operatorname{Maximal} P x \iff P x \land \forall \{y\}, x < y \rightarrow \neg P y $$$

Lean4

theorem maximal_iff_forall_gt : Maximal P x ↔ P x ∧ ∀ ⦃y⦄, x < y → ¬P y :=
  minimal_iff_forall_lt (α := αᵒᵈ)

Похожие утверждения