English
For f : α → α' → β, a ∈ α, a' ∈ α', b ∈ β, we have: uncurry (update f a (update (f a) a' b)) = update (uncurry f) (a, a') b.
Русский
Для f : α → α' → β, a ∈ α, a' ∈ α', b ∈ β: uncurry (update f a (update (f a) a' b)) = update (uncurry f) (a, a') b.
LaTeX
$$$ \\forall {f : \\alpha \\to \\alpha' \\to \\beta} {a : \\alpha} {a' : \\alpha'} {b : \\beta},\\n \\operatorname{uncurry}(\\operatorname{update} f a (\\operatorname{update} (f a) a' b)) = \\operatorname{update}(\\operatorname{uncurry} f) { fst := a, snd := a' } b$$$
Lean4
theorem uncurry_update_update {α α' β : Type*} [DecidableEq α] [DecidableEq α'] (f : α → α' → β) (a : α) (a' : α')
(b : β) : uncurry (Function.update f a (Function.update (f a) a' b)) = Function.update (uncurry f) (a, a') b :=
by
apply curry_injective
simp [curry_update]
