English
Equality between comp₂Measurable and compMeasurable holds when both sides use the pair construction.
Русский
Равенство между comp₂Measurable и compMeasurable сохраняется при использовании пары.
LaTeX
$$$comp₂Measurable\ g hg f₁ f₂ =\; compMeasurable\ (Function.uncurry g)\ hg\ (f₁.pair f₂)$$$
Lean4
/-- Given a measurable function `g : β → γ → δ`, and almost everywhere equal functions
`[f₁] : α →ₘ β` and `[f₂] : α →ₘ γ`, return the equivalence class of the function
`fun a => g (f₁ a) (f₂ a)`, i.e., the almost everywhere equal function
`[fun a => g (f₁ a) (f₂ a)] : α →ₘ γ`. This requires `δ` to have second-countable topology. -/
def comp₂Measurable (g : β → γ → δ) (hg : Measurable (uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) : α →ₘ[μ] δ :=
compMeasurable _ hg (f₁.pair f₂)
