rec0 — Mathlib

English

There exists a dependent eliminator for the empty finite type: for any family α : Fin 0 → Sort*, there is a function rec0 : ∀ i : Fin 0, α i.

Русский

Существует зависимая элиминация для пустого типа Fin 0: для любой семействной структуры α : Fin 0 → Sort* существует функция rec0 : ∀ i : Fin 0, α i.

LaTeX

$$$∃ α : Fin(0) \to \mathrm{Sort}^*,\ ∃ rec0 : \forall i : Fin(0), α(i).$$$

Lean4

/-- A dependent variant of `Fin.elim0`. -/
def rec0 {α : Fin 0 → Sort*} (i : Fin 0) : α i :=
  absurd i.2 (Nat.not_lt_zero _)

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