ne_iff_lt_or_gt

Mathlib.Order.Defs.LinearOrder

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

English

a ≠ b iff a < b or b < a.

Русский

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

LaTeX

$$$ a \ne b \\leftrightarrow a < b \\lor b < a $$$

Lean4

theorem ne_iff_lt_or_gt : a ≠ b ↔ a < b ∨ b < a :=
  ⟨lt_or_gt_of_ne, (Or.elim · ne_of_lt ne_of_gt)⟩

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

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

Разделы

Аффилиация

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