append_right_cons — Mathlib

English

Appending xs with cons y ys is the same as appending snoc xs y with ys up to a cast.

Русский

Добавление xs с cons y ys эквивалентно добавлению snoc xs y с ys с приведением.

LaTeX

$$$\\\\operatorname{append} xs (\\\\operatorname{cons} y \\\\; ys) = \\\\operatorname{append}(\\\\operatorname{snoc} xs y) ys \\\\circ \\\\operatorname{cast} (\\\\mathrm{Nat.succ\_add\_eq\_add\_succ} ..).$$$$

Lean4

theorem append_right_cons {n m} {α : Sort*} (xs : Fin n → α) (y : α) (ys : Fin m → α) :
    Fin.append xs (Fin.cons y ys) = Fin.append (Fin.snoc xs y) ys ∘ Fin.cast (Nat.succ_add_eq_add_succ ..).symm := by
  rw [append_left_snoc]; rfl

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