minimal_iff — Mathlib

English

A predicate P at x is Minimal if and only if P x holds and for every y with P y, if y ≤ x then x = y.

Русский

Миха минимальность P на x эквивалентна тому, что P x истинно и для любого y с P y, если y ≤ x, то x = y.

LaTeX

$$$ \operatorname{Minimal} P x \leftrightarrow P x \land \forall \{y\}, P y \rightarrow y \le x \rightarrow x = y $$$

Lean4

theorem minimal_iff : Minimal P x ↔ P x ∧ ∀ ⦃y⦄, P y → y ≤ x → x = y :=
  ⟨fun h ↦ ⟨h.1, fun _ ↦ h.eq_of_ge⟩, fun h ↦ ⟨h.1, fun _ hy hle ↦ (h.2 hy hle).le⟩⟩

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