comp₂Measurable_eq_mk — Mathlib

English

Equality with Measurable-Pair representation and pair representation coincide.

Русский

Согласование представления через измеримую пару и через пару однотипно.

LaTeX

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

Lean4

theorem comp₂Measurable_eq_mk (g : β → γ → δ) (hg : Measurable (uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
    comp₂Measurable g hg f₁ f₂ =
      mk (fun a => g (f₁ a) (f₂ a))
        (hg.comp_aemeasurable (f₁.aemeasurable.prodMk f₂.aemeasurable)).aestronglyMeasurable :=
  by rw [comp₂Measurable_eq_pair, pair_eq_mk, compMeasurable_mk]; rfl

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