toNat_rightInverse — Mathlib

English

The natural embedding into cardinals is a right-inverse of toNat, i.e., for all n ∈ ℕ, toNat(natCast(n)) = n.

Русский

Естественное вложение чисел в кардиналы является правой обратной к toNat: для всех n ∈ ℕ выполнено toNat(natCast(n)) = n.

LaTeX

$$$\forall n \in \mathbb{N}:\ toNat(\uparrow n) = n.$$$

Lean4

/-- `toNat` has a right-inverse: coercion. -/
theorem toNat_rightInverse : Function.RightInverse ((↑) : ℕ → Cardinal) toNat :=
  toNat_natCast

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