toENatAux_nat — Mathlib

English

The natural numbers embed into the extended natural numbers ℕ∞ as themselves; for every n ∈ ℕ, the image of n under the embedding agrees with n.

Русский

Натуральные числа встраиваются в расширенные натуральные числа ℕ∞ как сами по себе; для любого n ∈ ℕ образ n под встраиванием равен n.

LaTeX

$$$\\forall n \\in \\mathbb{N},\\; \\operatorname{toENatAux}(n) = n$$$

Lean4

theorem toENatAux_nat (n : ℕ) : toENatAux n = n :=
  Nat.cast_injective.extend_apply ..

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