LeanPool.RlTheoryInLean.MeasureTheory.MeasurableSpace.Constructions #
theorem
Measurable.of_uncurry
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{f : α → β → γ}
(h : Measurable (Function.uncurry f))
: