insertNth_removeNth — Mathlib

English

Removing a coordinate and then inserting a value at that coordinate yields the same as updating the original function at that coordinate.

Русский

Удаление координаты и затем вставка значения в эту координату дают тот же результат, что и обновление исходной функции в этой координате.

LaTeX

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

Lean4

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

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