not_minimal_iff — Mathlib

English

If P x holds, then not being Minimal P x is equivalent to the existence of a witness y with P y, y ≤ x, and not x ≤ y.

Русский

Если P x верно, то не являясь минимальным, существует элемент y с P y, y ≤ x и не x ≤ y.

LaTeX

$$$\\text{hx: } P x \\Rightarrow \\neg \\text{Minimal } P x \\iff \\exists y\\,(P y \\land y \\le x \\land \\neg (x \\le y))$$$

Lean4

theorem not_minimal_iff (hx : P x) : ¬Minimal P x ↔ ∃ y, P y ∧ y ≤ x ∧ ¬(x ≤ y) := by simp [Minimal, hx]

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