nilFun_comp

Mathlib.Data.TypeVec

URI: https://scilib.ai/kg/mathlib#TypeVec.nilFun_comp

English

Composing nilFun on the left with any f0 yields f0: nilFun ∘ f0 = f0.

Русский

Слева от nilFun стоит любая стрелa f0: nilFun ∘ f0 = f0.

LaTeX

$$$\mathrm{nilFun} \circ f_{0} = f_{0}$$$

Lean4

theorem nilFun_comp {α₀ : TypeVec 0} (f₀ : α₀ ⟹ Fin2.elim0) : nilFun ⊚ f₀ = f₀ :=
  funext Fin2.elim0

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

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

Разделы

Аффилиация

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