append_comp_sumElim — Mathlib

English

Fin.append xs ys composed with Sum.elim (Fin.castAdd) (Fin.natAdd) equals Sum.elim xs ys.

Русский

Для функций xs, ys из Fin м и Fin н, композиция Fin.append xs ys с Sum.elim (Fin.castAdd) (Fin.natAdd) равна Sum.elim xs ys.

LaTeX

$$$\\mathrm{Fin.append}\\ xs\\ ys \\circ \\mathrm{Sum.elim}(\\mathrm{Fin.castAdd}\\ _,\\ \\mathrm{Fin.natAdd}\\ _) = \\mathrm{Sum.elim}\\ xs ys.$$$

Lean4

theorem append_comp_sumElim {xs : Fin m → α} {ys : Fin n → α} :
    Fin.append xs ys ∘ Sum.elim (Fin.castAdd _) (Fin.natAdd _) = Sum.elim xs ys := by ext (i | j) <;> simp

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