not_lt

Mathlib.Order.Defs.LinearOrder

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

English

¬(a < b) iff b ≤ a.

Русский

¬(a < b) эквивалентно b ≤ a.

LaTeX

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

Lean4

@[simp, push]
theorem not_lt : ¬a < b ↔ b ≤ a :=
  ⟨le_of_not_gt, not_lt_of_ge⟩

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

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

Разделы

Аффилиация

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