append_castAdd_natAdd — Mathlib

English

The same as append_comp_rev but presented as an equality of functions after applying funext.

Русский

То же самое, что append_comp_rev, но записано как равенство функций после применения funext.

LaTeX

$$$\\mathrm{Function}.ext\\; (\\text{append_rev}_\\text{xs,ys})$ и т.д.$$

Lean4

theorem append_castAdd_natAdd {f : Fin (m + n) → α} : append (fun i ↦ f (castAdd n i)) (fun i ↦ f (natAdd m i)) = f :=
  by
  unfold append addCases
  simp

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