append_cast_left — Mathlib

English

For xs : Fin n → α, ys : Fin m → α, and h : n' = n, append (xs ∘ cast h) ys = (append xs ys) ∘ cast (by rw [h]).

Русский

Для xs : Fin n → α, ys : Fin m → α и h : n' = n, выполняется append (xs ∘ cast h) ys = (append xs ys) ∘ cast (по доказательству).

LaTeX

$$$\\mathrm{append}(\\mathrm{xs} \\circ \\mathrm{Fin.cast}\\, h)\ (\\mathrm{ys}) = \\mathrm{append}(\\mathrm{xs},\\mathrm{ys}) \\circ \\mathrm{Fin.cast}(\\text{by rw [h]}).$$$

Lean4

@[simp]
theorem append_cast_left {n m} (xs : Fin n → α) (ys : Fin m → α) (n' : ℕ) (h : n' = n) :
    Fin.append (xs ∘ Fin.cast h) ys = Fin.append xs ys ∘ (Fin.cast <| by rw [h]) := by subst h; simp

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