instCharZero — Mathlib

English

The natural numbers embed injectively into the ordinals via casting, i.e., distinct naturals map to distinct ordinals.

Русский

Натуральные числа вводятся в ординалы инъективно: различные натуральные числа задают разные ординалы.

LaTeX

$$$\forall m,n \in \mathbb{N},\ (m = n) \Rightarrow (m:\mathrm{Ordinal}) = (n:\mathrm{Ordinal})$$$

Lean4

instance instCharZero : CharZero Ordinal := by
  refine ⟨fun a b h ↦ ?_⟩
  rwa [← Cardinal.ord_nat, ← Cardinal.ord_nat, Cardinal.ord_inj, Nat.cast_inj] at h

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