snoc_zero — Mathlib

English

snoc_castAdd expresses the componentwise relationship between snoc and castAdd: (snoc f a) (Fin.castAdd (n+m) i) = f (Fin.castAdd m i).

Русский

snoc_castAdd выражает зависимость между snoc и castAdd: (snoc f a) (Fin.castAdd (n+m) i) = f (Fin.castAdd m i).

LaTeX

$$$\\forall {m n} {α} (f : Fin (n+m) → α) (a : α) (i : Fin n), (\\mathrm{snoc}\\ f a) (\\mathrm{castAdd}(m+1) i) = f (\\mathrm{castAdd} m i).$$$

Lean4

theorem snoc_zero {α : Sort*} (p : Fin 0 → α) (x : α) : Fin.snoc p x = fun _ ↦ x :=
  rfl

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