update_erase_eq_update — Mathlib

English

Updating after erasing at a equals updating the original: update (erase a f) a b = update f a b.

Русский

Обновление после стирания на позиции a эквивалентно обновлению исходной функции: update (erase a f) a b = update f a b.

LaTeX

$$update (erase a f) a b = update f a b$$

Lean4

@[simp]
theorem update_erase_eq_update (f : α →₀ M) (a : α) (b : M) : update (erase a f) a b = update f a b := by
  rw [erase_eq_update_zero, update_idem]

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