linearOrder

Mathlib.Data.Real.Basic

URI: https://scilib.ai/kg/mathlib#Real.linearOrder

English

Let R = ℝ equipped with its usual order; then (ℝ, ≤) is a linear ordering.

Русский

Пусть R = ℝ оснащено обычным порядком; тогда (ℝ, ≤) образует линейный порядок.

LaTeX

$$$\forall a,b\in\mathbb{R},\ a\le b \lor b\le a$$$

Lean4

noncomputable instance linearOrder : LinearOrder ℝ :=
  Lattice.toLinearOrder ℝ

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

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

Разделы

Аффилиация

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