append_right_nil — Mathlib

English

If n = 0, then append u v = u ∘ Fin.cast (by rw [hv, Nat.add_zero]).

Русский

Если n = 0, тогда append u v = u ∘ Fin.cast (по доказательству Nat.add_zero).

LaTeX

$$$\\text{append } u\\ v = u \\circ \\mathrm{Fin.cast}\\left(\\mathrm{Nat.add_zero}\\right).$$$

Lean4

theorem append_right_nil (u : Fin m → α) (v : Fin n → α) (hv : n = 0) :
    append u v = u ∘ Fin.cast (by rw [hv, Nat.add_zero]) :=
  by
  refine funext (Fin.addCases (fun l => ?_) fun r => ?_)
  · rw [append_left, Function.comp_apply]
    refine congr_arg u (Fin.ext ?_)
    simp
  · exact (Fin.cast hv r).elim0

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