prodMk_right — Mathlib

English

Reiterates the a.e.-measurability of the right-hand sections in the product measure setting.

Русский

Повторение: почти всюду секции справа измеримы.

LaTeX

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

Lean4

theorem prodMk_right [SFinite μ] [SFinite ν] {f : α × β → X} (hf : AEStronglyMeasurable f (μ.prod ν)) :
    ∀ᵐ y ∂ν, AEStronglyMeasurable (fun x => f (x, y)) μ :=
  hf.prod_swap.prodMk_left

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