recTopCoe_coe

Mathlib.Data.ENat.Defs

URI: https://scilib.ai/kg/mathlib#ENat.recTopCoe_coe

English

On a natural cast, recTopCoe gives f a: recTopCoe d f (↑a) = f a.

Русский

На случаи ↑a: recTopCoe d f (↑a) = f a.

LaTeX

$$$$ \\operatorname{recTopCoe} (d,f) (a.cast) = f(a) $$$$

Lean4

@[simp]
theorem recTopCoe_coe {C : ℕ∞ → Sort*} (d : C ⊤) (f : ∀ a : ℕ, C a) (x : ℕ) : @recTopCoe C d f ↑x = f x :=
  rfl

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

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

Разделы

Аффилиация

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