append_elim0 — Mathlib

English

The identity append u Fin.elim0 equals u composed with Fin.cast Nat.add_zero: append u Fin.elim0 = u ∘ Fin.cast (Nat.add_zero _).

Русский

Идентичность: append u Fin.elim0 = u ∘ Fin.cast (Nat.add_zero _).

LaTeX

$$$\\mathrm{append}\\;u\\;\\mathrm{Fin.elim0} = u \\circ \\mathrm{Fin.cast}(\\mathrm{Nat.add_zero}()).$$$

Lean4

@[simp]
theorem append_elim0 (u : Fin m → α) : append u Fin.elim0 = u ∘ Fin.cast (Nat.add_zero _) :=
  append_right_nil _ _ rfl

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