comp₂_eq_mk — Mathlib

English

The a.e.-equivalence of comp₂ g hg f₁ f₂ with the pointwise application of g holds.

Русский

Эквивалентность a.e. comp₂ через g сохраняется в точной форме.

LaTeX

$$$f.pair g =^{\mu}_{ae} (a \mapsto (f(a), g(a)))$$$

Lean4

theorem comp₂_eq_mk (g : β → γ → δ) (hg : Continuous (uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
    comp₂ g hg f₁ f₂ =
      mk (fun a => g (f₁ a) (f₂ a))
        (hg.comp_aestronglyMeasurable (f₁.aestronglyMeasurable.prodMk f₂.aestronglyMeasurable)) :=
  by rw [comp₂_eq_pair, pair_eq_mk, comp_mk]; rfl

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