typevecCasesNil₂ — Mathlib

English

The specialized_nil₂ case is compatible with appending a function; i.e., typevecCasesNil₂ f nilFun = f.

Русский

Специализированный случай Nil₂ совместим с операцией добавления; то есть typevecCasesNil₂ f nilFun = f.

LaTeX

$$$$\\mathrm{typevecCasesNil₂}\\ f\\ \\mathrm{nilFun} = f.$$$$

Lean4

/-- specialized cases distinction for an arrow in the category of 0-length type vectors -/
def typevecCasesNil₂ {β : Fin2.elim0 ⟹ Fin2.elim0 → Sort*} (f : β nilFun) : ∀ f, β f :=
  by
  intro g
  suffices g = nilFun by rwa [this]
  ext ⟨⟩

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