empty_eq — Mathlib

English

Let α be any type. There is a unique function from Fin(0) to α; consequently every function v: Fin(0) → α equals the empty function.

Русский

Пусть α — произвольный тип. Существует единственная функция из Fin(0) в α; следовательно, любая функция v: Fin(0) → α равна пустой функции.

LaTeX

$$$\forall {\alpha} \ (v : \mathrm{Fin} 0 \to \alpha),\ v = \text{vecEmpty}$$$

Lean4

theorem empty_eq (v : Fin 0 → α) : v = ![] :=
  Subsingleton.elim _ _

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