snoc_comp_castSucc — Mathlib

English

snoc f a composed with castSucc equals f composed with castSucc; i.e., (snoc f a) ∘ castSucc = f.

Русский

snoc f a после приведения castSucc эквивалентно f: (snoc f a) ∘ castSucc = f.

LaTeX

$$$\\big(\\mathrm{snoc}\\ f\\ a\\big) \\circ \\mathrm{castSucc} = f$$$

Lean4

@[simp]
theorem snoc_comp_castSucc {α : Sort*} {a : α} {f : Fin n → α} : (snoc f a : Fin (n + 1) → α) ∘ castSucc = f :=
  funext fun i ↦ by rw [Function.comp_apply, snoc_castSucc]

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