append_left_nil — Mathlib

English

If m = 0, then append u v = v ∘ Fin.cast (by rw [hu, Nat.zero_add]).

Русский

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

LaTeX

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

Lean4

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

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