isTotal

Mathlib.Order.RelClasses

URI: https://scilib.ai/kg/mathlib#LE.isTotal

English

In a linear order, ≤ is a total relation: any two elements are comparable by ≤.

Русский

В линейном порядке ≤ относится к полной сравнительности: любые два элемента сравнимы по ≤.

LaTeX

$$$\forall a,b \in \alpha,\ a \le b \lor b \le a$$$

Lean4

instance isTotal [LinearOrder α] : IsTotal α (· ≤ ·) :=
  ⟨le_total⟩

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

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

Разделы

Аффилиация

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