finZeroElim — Mathlib

English

There is an elimination principle for the empty finite type Fin 0: any function on Fin 0 is vacuous.

Русский

Существует принцип устранения для пустого множества Fin 0: любая функция на Fin 0 тривиальна/пустая.

LaTeX

$$$\\mathrm{finZeroElim} : {\\alpha : Fin 0 \\to \\mathrm{Sort}^*} \\to (x : Fin 0) \\to \\alpha x$ is defined by $x.elim0$$$

Lean4

/-- Elimination principle for the empty set `Fin 0`, dependent version. -/
def finZeroElim {α : Fin 0 → Sort*} (x : Fin 0) : α x :=
  x.elim0

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