α : Type u_4
β : Type u_2
γ : Type u_1
δ : Type u_3
inst✝¹⁵ : MeasurableSpace α
μ ν : Measure α
inst✝¹⁴ : TopologicalSpace β
inst✝¹³ : TopologicalSpace γ
inst✝¹² : TopologicalSpace δ
inst✝¹¹ : MeasurableSpace β
inst✝¹⁰ : PseudoMetrizableSpace β
inst✝⁹ : BorelSpace β
inst✝⁸ : SecondCountableTopology β
inst✝⁷ : MeasurableSpace γ
inst✝⁶ : PseudoMetrizableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : SecondCountableTopology γ
inst✝³ : MeasurableSpace δ
inst✝² : PseudoMetrizableSpace δ
inst✝¹ : OpensMeasurableSpace δ
inst✝ : SecondCountableTopology δ
g : β → γ → δ
hg : Measurable (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ ↑(mk (fun a => g (↑f₁ a) (↑f₂ a)) (_ : AEStronglyMeasurable (uncurry g ∘ fun x => (↑f₁ x, ↑f₂ x)) μ)) =ᵐ[μ] fun a =>
    g (↑f₁ a) (↑f₂ a)
α : Type u_4
β : Type u_2
γ : Type u_1
δ : Type u_3
inst✝¹⁵ : MeasurableSpace α
μ ν : Measure α
inst✝¹⁴ : TopologicalSpace β
inst✝¹³ : TopologicalSpace γ
inst✝¹² : TopologicalSpace δ
inst✝¹¹ : MeasurableSpace β
inst✝¹⁰ : PseudoMetrizableSpace β
inst✝⁹ : BorelSpace β
inst✝⁸ : SecondCountableTopology β
inst✝⁷ : MeasurableSpace γ
inst✝⁶ : PseudoMetrizableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : SecondCountableTopology γ
inst✝³ : MeasurableSpace δ
inst✝² : PseudoMetrizableSpace δ
inst✝¹ : OpensMeasurableSpace δ
inst✝ : SecondCountableTopology δ
g : β → γ → δ
hg : Measurable (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ ↑(comp₂Measurable g hg f₁ f₂) =ᵐ[μ] fun a => g (↑f₁ a) (↑f₂ a)
rw [comp₂Measurable_eq_mk]
no goals
α : Type u_4
β : Type u_2
γ : Type u_1
δ : Type u_3
inst✝¹⁵ : MeasurableSpace α
μ ν : Measure α
inst✝¹⁴ : TopologicalSpace β
inst✝¹³ : TopologicalSpace γ
inst✝¹² : TopologicalSpace δ
inst✝¹¹ : MeasurableSpace β
inst✝¹⁰ : PseudoMetrizableSpace β
inst✝⁹ : BorelSpace β
inst✝⁸ : SecondCountableTopology β
inst✝⁷ : MeasurableSpace γ
inst✝⁶ : PseudoMetrizableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : SecondCountableTopology γ
inst✝³ : MeasurableSpace δ
inst✝² : PseudoMetrizableSpace δ
inst✝¹ : OpensMeasurableSpace δ
inst✝ : SecondCountableTopology δ
g : β → γ → δ
hg : Measurable (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ ↑(mk (fun a => g (↑f₁ a) (↑f₂ a)) (_ : AEStronglyMeasurable (uncurry g ∘ fun x => (↑f₁ x, ↑f₂ x)) μ)) =ᵐ[μ] fun a =>
    g (↑f₁ a) (↑f₂ a)
apply coeFn_mk