not_minimal_iff_exists_lt — Mathlib

English

Given P and x with P x, not Minimal P x is equivalent to the existence of a y with y < x and P y.

Русский

Если P x истинно, то Not Minimal P x эквивално существованию y с y < x и P y.

LaTeX

$$$ P x \rightarrow \bigl( \neg \operatorname{Minimal} P x \iff \exists y, y < x \land P y \bigr) $$$

Lean4

theorem not_minimal_iff_exists_lt (hx : P x) : ¬Minimal P x ↔ ∃ y, y < x ∧ P y := by
  simp_rw [not_minimal_iff hx, lt_iff_le_not_ge, and_comm]

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