prodMk_left — Mathlib

English

Symmetric version: for a.e. y, the map x ↦ f(x,y) is AEStronglyMeasurable on α.

Русский

Симметричная версия: почти всюду y, карта x↦f(x,y) измерима на α.

LaTeX

$$$$\\forall^{\\text{ae}} y,\\; \\text{AEStronglyMeasurable}(x\\mapsto f(x,y))\\;\\text{на } α$$$$

Lean4

theorem prodMk_left [SFinite ν] {f : α × β → X} (hf : AEStronglyMeasurable f (μ.prod ν)) :
    ∀ᵐ x ∂μ, AEStronglyMeasurable (fun y => f (x, y)) ν :=
  by
  filter_upwards [ae_ae_of_ae_prod hf.ae_eq_mk] with x hx
  exact ⟨fun y ↦ hf.mk f (x, y), hf.stronglyMeasurable_mk.comp_measurable measurable_prodMk_left, hx⟩

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