not_isMax_iff

Mathlib.Order.Max

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

English

Not IsMax a iff there exists b with a < b.

Русский

Не IsMax a эквивалентно существованию b, такого что a < b.

LaTeX

$$$\\\\lnot \\\\mathrm{IsMax}(a) \\\\leftrightarrow \\\\exists b, \\\\ a < b$$$

Lean4

@[simp]
theorem not_isMax_iff : ¬IsMax a ↔ ∃ b, a < b := by simp [lt_iff_le_not_ge, IsMax, not_forall]

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

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

Разделы

Аффилиация

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