recTopCoe_top

Mathlib.Data.ENat.Defs

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

English

The evaluation of recTopCoe on ⊤ equals the top-level value d: recTopCoe d f ⊤ = d.

Русский

Применение recTopCoe к ⊤ даёт верхнее значение d: recTopCoe d f ⊤ = d.

LaTeX

$$$$ \\operatorname{recTopCoe} (d,f)(\\top) = d $$$$

Lean4

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

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

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

Разделы

Аффилиация

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