comp₂Measurable_eq_pair — Mathlib

English

Equality between the two representations reduces to equality of MK representations with product measurability data.

Русский

Сведение равенств к MK-представлениям с данными произведения измеримости.

LaTeX

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

Lean4

theorem comp₂Measurable_eq_pair (g : β → γ → δ) (hg : Measurable (uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
    comp₂Measurable g hg f₁ f₂ = compMeasurable _ hg (f₁.pair f₂) :=
  rfl

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