ofNat_nat

Mathlib.Logic.Denumerable

URI: https://scilib.ai/kg/mathlib#Denumerable.ofNat_nat

English

For every n, the nth element of ℕ equals n.

Русский

Для каждого n n-й элемент ℕ равен n.

LaTeX

$$$ \operatorname{ofNat} \mathbb{N} \ n = n $$$

Lean4

@[simp]
theorem ofNat_nat (n) : ofNat ℕ n = n :=
  rfl

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

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

Разделы

Аффилиация

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