map_uncurry — Mathlib

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

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