coeFn_comp₂Measurable — Mathlib

English

Equality of comp₂Measurable in mk-mk form yields MK from the pointwise g, with the same measurability data.

Русский

Равенство comp₂Measurable в mk mk форме даёт MK от покомпонентной функции.

LaTeX

$$$comp₂Measurable\ g hg (mk f₁ hf₁) (mk f₂ hf₂) = mk(\lambda a, g (f₁ a) (f₂ a)) \ (hg.comp_aemeasurable (hf₁.aemeasurable.prodMk hf₂.aemeasurable))$$$

Lean4

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

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