toNatHom_apply

Mathlib.Data.ENat.Basic

URI: https://scilib.ai/kg/mathlib#ENat.toNatHom_apply

English

For every n ∈ ℕ, toNatHom n = toNat n.

Русский

Для любого n ∈ ℕ выполняется toNatHom n = toNat n.

LaTeX

$$$\\\\forall n \\\\in \\\\mathbb{N},\\\\ toNatHom(n) = toNat(n).$$$

Lean4

theorem toNatHom_apply (n : ℕ) : toNatHom n = toNat n :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru