not_le

Mathlib.Order.Defs.LinearOrder

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

English

¬(a ≤ b) ⇔ b < a.

Русский

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

LaTeX

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

Lean4

@[simp, push]
theorem not_le : ¬a ≤ b ↔ b < a :=
  lt_iff_not_ge.symm

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

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

Разделы

Аффилиация

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