English
Let f be a finitely supported function f: α →₀ M. For any a ∈ α and b, c ∈ M, updating f at a first to b and then again at a to c yields the same as updating f at a to c. In symbols: update(update f a b) a c = update f a c.
Русский
Пусть f: α →₀ M имеет конечную опору. Для любого a ∈ α и b, c ∈ M, последовательное обновление в точке a сначала до b, затем до c даёт такое же значение, как обновление до c напрямую: update(update f a b) a c = update f a c.
LaTeX
$$$ \forall f:\alpha \to_0 M,\ a\in\alpha,\ b,c\in M:\ update(update\, f\, a\, b)\ a\ c = update\, f\, a\, c $$$
Lean4
@[simp]
theorem update_idem (f : α →₀ M) (a : α) (b c : M) : update (update f a b) a c = update f a c :=
letI := Classical.decEq α
DFunLike.coe_injective <| Function.update_idem _ _ _
