append_left' — Mathlib

English

A variant of the left-append identity using Fin.castLE instead of Fin.castAdd: append u v (Fin.castLE i) = u i.

Русский

Вариант левого добавления с использованием Fin.castLE вместо Fin.castAdd: append u v (Fin.castLE i) = u i.

LaTeX

$$$\\mathrm{append}(u,v)(\\mathrm{Fin.castLE} (\\text{..})\\ i) = u(i).$$$

Lean4

/-- Variant of `append_left` using `Fin.castLE` instead of `Fin.castAdd`. -/
@[simp]
theorem append_left' (u : Fin m → α) (v : Fin n → α) (i : Fin m) : append u v (Fin.castLE (by cutsat) i) = u i :=
  addCases_left _

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