eq_iff_not_lt_of_le

Mathlib.Order.Basic

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

English

If a ≤ b, then a = b is equivalent to not(a < b).

Русский

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

LaTeX

$$$ (a \le b) \to (a = b \iff \lnot (a < b)) $$$

Lean4

@[deprecated LE.le.not_lt_iff_eq (since := "2025-06-08")]
theorem eq_iff_not_lt_of_le (hab : a ≤ b) : a = b ↔ ¬a < b :=
  hab.not_lt_iff_eq.symm

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

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

Разделы

Аффилиация

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