English
Given a continuous two-variable function g, and two μ-a.e.-equal maps into β and γ, the composition f₁.pair f₂ passed through g is an a.e.-equal map into δ.
Русский
Для непрерывной функции g(β, γ) и двух функций f₁, f₂ равных почти повсюду, композиция через g задаёт новый AEFun в δ.
LaTeX
$$$comp\₂(g,hg,f₁,f₂) : α →ₘ[μ] δ$ defined by $a \mapsto g(f₁(a), f₂(a))$.$$
Lean4
/-- Given a continuous 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)] : α →ₘ γ` -/
def comp₂ (g : β → γ → δ) (hg : Continuous (uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) : α →ₘ[μ] δ :=
comp _ hg (f₁.pair f₂)
