lt_of_le_not_ge

Mathlib.Order.Defs.PartialOrder

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

English

If a ≤ b and not(b ≤ a), then a < b.

Русский

Если a ≤ b и не (b ≤ a), то a < b.

LaTeX

$$$a \\le b \\\\land \\\\lnot (b \\le a) \\\\Rightarrow a < b$$$

Lean4

theorem lt_of_le_not_ge (hab : a ≤ b) (hba : ¬b ≤ a) : a < b :=
  lt_iff_le_not_ge.2 ⟨hab, hba⟩

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

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

Разделы

Аффилиация

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