toOrdinal_natCast

Mathlib.SetTheory.Ordinal.NaturalOps

URI: https://scilib.ai/kg/mathlib#NatOrdinal.toOrdinal_natCast

← MathLib Explorer

English

For every natural number n, toOrdinal n equals n.

Русский

Для каждого натурального числа n применяемое отображение toOrdinal возвращает n.

LaTeX

$$$$ \text{toOrdinal}(n) = n $$$$

Lean4

@[simp]
theorem toOrdinal_natCast (n : ℕ) : toOrdinal n = n := by
  induction n with
  | zero => rfl
  | succ n hn =>
    change (toOrdinal n) ♯ 1 = n + 1
    rw [hn]; exact nadd_one n

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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