insertNth_comp_succAbove — Mathlib

English

Inserting at i and then applying succAbove is equivalent to the identity on the tail: (insertNth i x p) ∘ i.succAbove = p.

Русский

После вставки на позицию i применение succAbove даёт исходный хвост: (insertNth i x p) ∘ i.succAbove = p.

LaTeX

$$$(insertNth\ i\ x\ p) \circ i.\\succAbove = p$$$

Lean4

@[simp]
theorem insertNth_comp_succAbove (i : Fin (n + 1)) (x : β) (p : Fin n → β) : insertNth i x p ∘ i.succAbove = p :=
  funext (insertNth_apply_succAbove i _ _)

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