recTopCoe_zero

Mathlib.Data.ENat.Basic

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

English

For any C, d ∈ C ⊤ and f : ∀ a ∈ ℕ, C a, recTopCoe d f 0 = f 0.

Русский

Для любого C, d ∈ C ⊤ и f : ∀ a ∈ ℕ, C a, recTopCoe d f 0 = f 0.

LaTeX

$$$\\\\forall {C : ENat \\\\to \\\\text{Sort}*} (d : C \\\\top) (f : \\\\forall a : \\\\mathbb{N}, C a), \\\\operatorname{recTopCoe} d f 0 = f 0.$$$

Lean4

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

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

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

Разделы

Аффилиация

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