not_lt

Mathlib.Order.Max

URI: https://scilib.ai/kg/mathlib#IsMax.not_lt

English

If a is maximal, then for all b, not a < b.

Русский

Если a максимален, то для любого b не выполняется a < b.

LaTeX

$$$\\\\mathrm{IsMax}(a) \\\\rightarrow \\\\lnot (a < b)$$$

Lean4

theorem not_lt (h : IsMax a) : ¬a < b := fun hb => hb.not_ge <| h hb.le

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

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

Разделы

Аффилиация

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