lt_iff_not_ge

Mathlib.Order.Defs.LinearOrder

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

English

a < b iff not b ≤ a.

Русский

a < b тогда и только тогда, когда не выполняется b ≤ a.

LaTeX

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

Lean4

theorem lt_iff_not_ge : a < b ↔ ¬b ≤ a :=
  ⟨not_le_of_gt, lt_of_not_ge⟩

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

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

Разделы

Аффилиация

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