toENat_comp_ofENat

Mathlib.SetTheory.Cardinal.ENat

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

English

Composing toENat with the canonical embedding of ENat into Cardinal yields the identity on ENat.

Русский

Составление toENat после канонического включения ENat в Cardinal даёт тождественный отображение на ENat.

LaTeX

$$$\\operatorname{toENat} \\circ (\\uparrow) = \\mathrm{id}$$$

Lean4

@[simp]
theorem toENat_comp_ofENat : toENat ∘ (↑) = id :=
  funext toENat_ofENat

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

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

Разделы

Аффилиация

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