toENatAux_ofENat

Mathlib.SetTheory.Cardinal.ENat

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

English

For every ENat value n, applying toENatAux returns the same value: toENatAux(n) = n.

Русский

Для каждого значения ENat применение toENatAux даёт то же самое значение: toENatAux(n) = n.

LaTeX

$$$\\forall n \\; (n : \\mathbb{N}^\\infty),\\; \\operatorname{toENatAux}(n) = n$$$

Lean4

theorem toENatAux_ofENat : ∀ n : ℕ∞, toENatAux n = n
  | (n : ℕ) => toENatAux_nat n
  | ⊤ => toENatAux_eq_top le_rfl

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

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

Разделы

Аффилиация

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