eq_nilFun — Mathlib

English

The 0-length identity arrow f equals nilFun; any arrow between zero-length TypeVecs is the same as the canonical nilFun.

Русский

Стрела между нулевой длиной TypeVec совпадает с nilFun; любое такое отображение равно канонической nilFun.

LaTeX

$$$$\\forall {\\alpha,\\beta : TypeVec(0)} (f : \\alpha ⟹ \\beta), f = nilFun.$$$$

Lean4

theorem eq_nilFun {α β : TypeVec 0} (f : α ⟹ β) : f = nilFun := by ext x; cases x

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