isMax_iff_forall_not_lt

Mathlib.Order.Max

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

English

IsMax a iff for all b, not a < b.

Русский

IsMax a эквивалентно тому, что для всех b не выполняется a < b.

LaTeX

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

Lean4

theorem isMax_iff_forall_not_lt : IsMax a ↔ ∀ b, ¬a < b :=
  ⟨fun h _ => h.not_lt, fun h _ hba => of_not_not fun hab => h _ <| hba.lt_of_not_ge hab⟩

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

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

Разделы

Аффилиация

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