minimal_iff_forall_lt — Mathlib

English

In a preorder, minimal P x is equivalent to P x together with the property that no y strictly precedes x satisfies P y.

Русский

В порядке предварения минимальность P у x эквивалентна P x и тому, что не существует y, меньшего x, такого что P y.

LaTeX

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

Lean4

theorem minimal_iff_forall_lt : Minimal P x ↔ P x ∧ ∀ ⦃y⦄, y < x → ¬P y := by simp [Minimal, lt_iff_le_not_ge, imp.swap]

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