instLinearOrder — Mathlib

English

The natural numbers are totally ordered by the usual ≤ relation; for any a,b ∈ ℕ, either a ≤ b or b ≤ a.

Русский

Натуральные числа образуют тотальный (линейный) порядок по отношению ≤: для любых a,b ∈ ℕ верно a ≤ b или b ≤ a.

LaTeX

$$$\forall a,b \in \mathbb{N},\; a \le b \lor b \le a.$$$

Lean4

instance instLinearOrder : LinearOrder ℕ where
  le := Nat.le
  le_refl := @Nat.le_refl
  le_trans := @Nat.le_trans
  le_antisymm := @Nat.le_antisymm
  le_total := @Nat.le_total
  lt := Nat.lt
  lt_iff_le_not_ge := @Nat.lt_iff_le_not_le
  toDecidableLT := inferInstance
  toDecidableLE := inferInstance
  toDecidableEq := inferInstance

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