update_eq_erase_add_single — Mathlib

English

Updating f at a by b can be decomposed as erasing the position a from f and then adding a new basis element at a with coefficient b.

Русский

Обновление f в позиции a на b можно разложить как удаление позиции a из f и затем добавление базисного элемента в позиции a с коэффициентом b.

LaTeX

$$$f.update\\ a\\ b = f.erase\\ a + single\\ a\\ b$$$

Lean4

theorem update_eq_erase_add_single : f.update a b = f.erase a + single a b := by
  classical ext x; by_cases hx : x = a <;> aesop (add norm coeff_single_apply)

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