insertNth_update — Mathlib

English

Inserting after updating is the same as updating after inserting.

Русский

Вставка после обновления эквивалентна обновлению после вставки.

LaTeX

$$$$ \mathrm{insertNth}\ x (\mathrm{update} f i y) = \mathrm{update} (\mathrm{insertNth}\ x f) (\mathrm{succAbove}\ i) y $$$$

Lean4

@[simp]
theorem insertNth_update (p : Fin (n + 1)) (x : α p) (i : Fin n) (y : α (p.succAbove i)) (f : ∀ j, α (p.succAbove j)) :
    p.insertNth x (update f i y) = update (p.insertNth x f) (p.succAbove i) y := by simp [insertNth_eq_iff]

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