ofENat_nat

Mathlib.SetTheory.Cardinal.ENat

URI: https://scilib.ai/kg/mathlib#Cardinal.ofENat_nat

English

For any natural number n, ofENat(n.cast) equals n.cast in cardinal.

Русский

Для любого натурального числа n отображение ofENat(n.cast) равно n.cast в кардиналах.

LaTeX

$$ofENat(n.cast) = n.cast$$

Lean4

@[simp, norm_cast]
theorem ofENat_nat (n : ℕ) : ofENat n = n :=
  rfl

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

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

Разделы

Аффилиация

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