leTotal_R — Mathlib

English

The order on the real numbers is total: for any a,b ∈ ℝ, either a ≤ b or b ≤ a.

Русский

Порядок на вещественных тотален: для любых a,b ∈ ℝ либо a ≤ b, либо b ≤ a.

LaTeX

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

Lean4

instance leTotal_R : IsTotal ℝ (· ≤ ·) :=
  ⟨by
    intro a b
    induction a using Real.ind_mk
    induction b using Real.ind_mk
    simpa using CauSeq.le_total ..⟩

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