ne_iff_lt_iff_le

Mathlib.Order.Basic

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

English

With decidable equality, the same equivalence holds: (a ≠ b ↔ a < b) ↔ a ≤ b.

Русский

При разрешимой эквивалентности равенствa та же эквивалентность: (a ≠ b ↔ a < b) ↔ a ≤ b.

LaTeX

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

Lean4

@[simp]
theorem ne_iff_lt_iff_le : (a ≠ b ↔ a < b) ↔ a ≤ b :=
  haveI := Classical.dec
  Decidable.ne_iff_lt_iff_le

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

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

Разделы

Аффилиация

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