removeNth_update — Mathlib

English

Updating at the removed coordinate has no effect on the remaining coordinates.

Русский

Обновление на удаляемой координате не влияет на остальные координаты.

LaTeX

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

Lean4

@[simp]
theorem removeNth_update (p : Fin (n + 1)) (x) (f : ∀ j, α j) : removeNth p (update f p x) = removeNth p f := by ext i;
  simp [removeNth]

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