nilElim — Mathlib

English

For any C that assigns a type to each vector, if H0 : C([]) and v : Vector3 α 0, then nilElim(H0,v) is a term of type C(v) obtained by substituting v with [].

Русский

Для любого C, присваивающего тип каждому вектору, если H0 : C([]) и v : Vector3 α 0, то nilElim(H0,v) имеет тип C(v), полученный подстановкой v в [].

LaTeX

$$$ \mathrm{nilElim}_{C}(H,v) = H \quad \text{(since } v=[]) $$$

Lean4

/-- Eliminator for an empty vector. -/
@[elab_as_elim]
def nilElim {C : Vector3 α 0 → Sort u} (H : C []) (v : Vector3 α 0) : C v := by rw [eq_nil v]; apply H

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