English
Let α be a type, β a family of types indexed by α, and f: α → β(a). If a ≠ b in α, and v ∈ β(a), w ∈ β(b), then updating f first at a to v and then at b to w yields the same function as updating first at b to w and then at a to v.
Русский
Пусть α — множество, β — семейство множеств, индексируемое по α, и функция f: α → β(a). При различиях a ≠ b в α и элементах v ∈ β(a), w ∈ β(b) последовательности обновлений функции дают одну и ту же функцию: сначала обновляем по a на v, потом по b на w, или наоборот.
LaTeX
$$$a \neq b \rightarrow \operatorname{update}(\operatorname{update} f\ a\ v)\ b\ w = \operatorname{update}(\operatorname{update} f\ b\ w)\ a\ v$$$
Lean4
theorem update_comm {α} [DecidableEq α] {β : α → Sort*} {a b : α} (h : a ≠ b) (v : β a) (w : β b) (f : ∀ a, β a) :
update (update f a v) b w = update (update f b w) a v :=
by
funext c
simp only [update]
by_cases h₁ : c = b <;> by_cases h₂ : c = a
· rw [dif_pos h₁, dif_pos h₂]
cases h (h₂.symm.trans h₁)
· rw [dif_pos h₁, dif_pos h₁, dif_neg h₂]
· rw [dif_neg h₁, dif_neg h₁]
· rw [dif_neg h₁, dif_neg h₁]
