not_maximal_iff_exists_gt

Mathlib.Order.Minimal

URI: https://scilib.ai/kg/mathlib#not_maximal_iff_exists_gt

English

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

Русский

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

LaTeX

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

Lean4

theorem not_maximal_iff_exists_gt (hx : P x) : ¬Maximal P x ↔ ∃ y, x < y ∧ P y :=
  not_minimal_iff_exists_lt (α := αᵒᵈ) hx

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru