lt_trichotomy

Mathlib.Order.Defs.LinearOrder

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

English

For any a,b in a linear order, exactly one of a < b, a = b, or b < a holds.

Русский

Для любых a,b в линейном порядке верно либо a < b, либо a = b, либо b < a.

LaTeX

$$$a < b \\lor a = b \\lor b < a$$$

Lean4

theorem lt_trichotomy (a b : α) : a < b ∨ a = b ∨ b < a := by grind [le_total, Decidable.lt_or_eq_of_le]

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

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

Разделы

Аффилиация

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