erase_update_eq_erase — Mathlib

English

Erasing after updating at the same index removes the update: erase a (update f a b) = erase a f.

Русский

Стирание после обновления на одинаковом индексе удаляет обновление: erase a (update f a b) = erase a f.

LaTeX

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

Lean4

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

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