English
Uncurrying a function corresponds to mapping over the pair-projection of an option containing a pair.
Русский
Развёртывание каррированной функции соответствует отображению над парой внутри опции.
LaTeX
$$$ \mathrm{map}\ (\mathrm{Function.uncurry}\ f)\ x = \mathrm{map}_2 f (\mathrm{map}\ Prod.fst\ x) (\mathrm{map}\ Prod.snd\ x) $$$
Lean4
@[simp]
theorem map_uncurry (f : α → β → γ) (x : Option (α × β)) :
x.map (uncurry f) = map₂ f (x.map Prod.fst) (x.map Prod.snd) := by grind