take_zero — Mathlib

English

Taking zero elements from a Fin-indexed vector yields the empty function; the result is the canonical elimination to the empty index.

Русский

Взятие нулевых элементов из вектора, индексированного Fin, даёт пустую функцию; результат соответствует каноническому исключению из пустого индекса.

LaTeX

$$$\mathrm{take}\;0\; n.zero\;le\; v = (\lambda i. \mathrm{elim0}\; i)$$$

Lean4

@[simp]
theorem take_zero (v : (i : Fin n) → α i) : take 0 n.zero_le v = fun i ↦ elim0 i := by ext i; exact elim0 i

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