elim0

Mathlib.Data.Fin.Fin2

URI: https://scilib.ai/kg/mathlib#Fin2.elim0

English

There are no elements of Fin2 0, so a dependent eliminator exists vacuously on Fin2 0.

Русский

У Fin2 0 нет элементов, значит любая зависимая элиминация по Fin2 0 тривиальна (пустой тип).

LaTeX

$$$\forall i : \mathrm{Fin2}(0),\; C(i)$$$

Lean4

/-- Ex falso. The dependent eliminator for the empty `Fin2 0` type. -/
def elim0 {C : Fin2 0 → Sort u} : ∀ i : Fin2 0, C i :=
  nofun

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

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

Разделы

Аффилиация

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