take_apply — Mathlib

English

For all m ≤ n and v: Fin n → α i, and i ∈ Fin m, the equality (take m h v)(i) = v(castLE h i) holds, i.e., take computes the first m coordinates by evaluating v at the embedded index.

Русский

Пусть m ≤ n и v: Fin n → α. Тогда для любого i ∈ Fin m выполняется (take m h v)(i) = v(castLE h i); take вычисляет первые m координат как отображение, получаемое из v через вложение.

LaTeX

$$$$\forall i:\mathrm{Fin}(m),\ (\mathrm{take}\ m\ h\ v)(i) = v(\mathrm{castLE}\ h\ i). $$$$

Lean4

@[simp]
theorem take_apply (m : ℕ) (h : m ≤ n) (v : (i : Fin n) → α i) (i : Fin m) : (take m h v) i = v (castLE h i) :=
  rfl

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