lt_of_le'

Mathlib.Order.Basic

URI: https://scilib.ai/kg/mathlib#Ne.lt_of_le'

English

If b ≠ a and a ≤ b, then a < b.

Русский

Если b ≠ a и a ≤ b, тогда a < b.

LaTeX

$$$ b \neq a \to a \le b \to a < b $$$

Lean4

theorem lt_of_le' : b ≠ a → a ≤ b → a < b :=
  flip lt_of_le_of_ne'

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

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

Разделы

Аффилиация

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