lt_or_lt_iff_ne

Mathlib.Order.Basic

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

English

In a linear order, a < b or b < a iff a ≠ b.

Русский

В линейном порядке либо a < b, либо b < a эквивалентно a ≠ b.

LaTeX

$$$a < b \\lor b < a \\iff a \\neq b$$$

Lean4

/-- A version of `ne_iff_lt_or_gt` with LHS and RHS reversed. -/
@[simp]
theorem lt_or_lt_iff_ne : a < b ∨ b < a ↔ a ≠ b :=
  ne_iff_lt_or_gt.symm

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

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

Разделы

Аффилиация

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