not_maximal_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem not_maximal_iff (hx : P x) : ¬Maximal P x ↔ ∃ y, P y ∧ x ≤ y ∧ ¬(y ≤ x) :=
  not_minimal_iff (α := αᵒᵈ) hx

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