eq_iff_le_not_lt

Mathlib.Order.Basic

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

English

a = b iff a ≤ b and not a < b.

Русский

a = b эквивалентно a ≤ b и не a < b.

LaTeX

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

Lean4

theorem eq_iff_le_not_lt : a = b ↔ a ≤ b ∧ ¬a < b :=
  open scoped Classical in Decidable.eq_iff_le_not_lt

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

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

Разделы

Аффилиация

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