English
Let f : α × α' → β, aa' = (a,a') ∈ α × α', and b ∈ β. Then curry (update f aa' b) = update (curry f) a (update (curry f a) a' b).
Русский
Пусть f : α × α' → β, aa' = (a,a') ∈ α × α', и b ∈ β. Тогда curry (update f aa' b) = update (curry f) a (update (curry f a) a' b).
LaTeX
$$$ \\forall {f : \\alpha \\times \\alpha' \\to \\beta} {aa' : \\alpha \\times \\alpha'} {b : \\beta},\\n \\operatorname{curry}(\\operatorname{update} f\\ aa' b) = \\operatorname{update}(\\operatorname{curry} f) aa'.1 (\\operatorname{update}(\\operatorname{curry} f aa'.1) aa'.2 b) $$$
Lean4
theorem curry_update {α α' β : Type*} [DecidableEq α] [DecidableEq α'] (f : α × α' → β) (aa' : α × α') (b : β) :
curry (Function.update f aa' b) = Function.update (curry f) aa'.1 (Function.update (curry f aa'.1) aa'.2 b) :=
by
ext a a'
let ⟨a₂, a₂'⟩ := aa'
obtain rfl | ha := eq_or_ne a a₂ <;> obtain rfl | ha' := eq_or_ne a' a₂' <;> simp [*]
