not_isMax_iff_ne_top

Mathlib.Order.BoundedOrder.Basic

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

English

Not IsMax a iff a ≠ ⊤.

Русский

Не IsMax a эквивалентно a ≠ ⊤.

LaTeX

$$$\neg\mathrm{IsMax}(a) \iff a \neq \top$$$

Lean4

theorem not_isMax_iff_ne_top : ¬IsMax a ↔ a ≠ ⊤ :=
  isMax_iff_eq_top.not

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

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

Разделы

Аффилиация

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