coeFn_comp₂ — Mathlib

English

When g is measurable and the two input maps are measurable in the ae-sense, the resulting function is measurable in the appropriate σ-algebra and equals compMeasurable g hg (f₁.pair f₂).

Русский

Если g измеримо, а два входных отображения измеримы как ae-функции, получившаяся функция измерима и равна compMeasurable g hg (f₁.pair f₂).

LaTeX

$$$comp₂Measurable\ g\ hg\ f₁\ f₂ = compMeasurable\ _ g\ hg (f₁.pair f₂)$$$

Lean4

theorem coeFn_comp₂ (g : β → γ → δ) (hg : Continuous (uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
    comp₂ g hg f₁ f₂ =ᵐ[μ] fun a => g (f₁ a) (f₂ a) :=
  by
  rw [comp₂_eq_mk]
  apply coeFn_mk

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