removeNth_update_succAbove — Mathlib

English

Removing at p and then updating at the position that follows p corresponds to updating at i after removing p.

Русский

Удаление на позиции p и затем обновление на следующей за p позиции эквивалентны обновлению на позиции i после удаления p.

LaTeX

$$$$ \mathrm{removeNth}\ p\ (\mathrm{update}\ f\ (\mathrm{p.succAbove}\ i)\ x) = \mathrm{update}\ (\mathrm{removeNth}\ p\ f)\ i\ x $$$$

Lean4

@[simp]
theorem removeNth_update_succAbove (p : Fin (n + 1)) (i : Fin n) (x : α (p.succAbove i)) (f : ∀ j, α j) :
    removeNth p (update f (p.succAbove i) x) = update (removeNth p f) i x :=
  by
  ext j
  rcases eq_or_ne j i with rfl | hne <;> simp [removeNth, *]

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