update_comm — Mathlib

English

For distinct a1 ≠ a2, updating f at a1 then a2 equals updating at a2 then a1.

Русский

Для разных a1 ≠ a2 обновление f по a1, затем по a2 эквивалентно обновлению по a2, затем по a1.

LaTeX

$$$update (update\ f\ a_1\ m_1)\ a_2\ m_2 = update (update\ f\ a_2\ m_2)\ a_1\ m_1$$$

Lean4

theorem update_comm (f : α →₀ M) {a₁ a₂ : α} (h : a₁ ≠ a₂) (m₁ m₂ : M) :
    update (update f a₁ m₁) a₂ m₂ = update (update f a₂ m₂) a₁ m₁ :=
  letI := Classical.decEq α
  DFunLike.coe_injective <| Function.update_comm h _ _ _

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