ofNat_lt — Mathlib

English

Let α be an ordered ring. The natural embedding of the natural numbers into α is order-preserving: for all m,n ∈ ℕ, (m : α) < (n : α) if and only if m < n.

Русский

Пусть α — упорядоченное кольцо. Натуральное внедрение ℕ в α сохраняет порядок: для любых m,n ∈ ℕ верно (m : α) < (n : α) тогда и только тогда m < n.

LaTeX

$$$ (m : \alpha) < (n : \alpha) \iff m < n $$$

Lean4

theorem ofNat_lt : (ofNat(m) : α) < (ofNat(n) : α) ↔ (OfNat.ofNat m : ℕ) < OfNat.ofNat n :=
  cast_lt

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