lt_of_not_ge

Mathlib.Order.Defs.LinearOrder

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

English

If not b ≤ a then a < b.

Русский

Если не выполняется b ≤ a, то a < b.

LaTeX

$$$ \\neg(b \\le a) \\rightarrow a < b$$$

Lean4

theorem lt_of_not_ge (h : ¬b ≤ a) : a < b :=
  lt_of_le_not_ge (le_of_not_ge h) h

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

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

Разделы

Аффилиация

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