aestronglyMeasurable_condExpL2 — Mathlib

English

For f: α →₂[μ] E, aestronglyMeasurable_condExpL2 holds: AEStronglyMeasurable (condExpL2 E 𝕜 hm f) μ.

Русский

Для f: α →₂[μ] E выполняется aestronglyMeasurable_condExpL2: AEStronglyMeasurable (condExpL2 E 𝕜 hm f) μ.

LaTeX

$$AEStronglyMeasurable[m](condExpL2 E 𝕜 hm f) μ$$

Lean4

theorem aestronglyMeasurable_condExpL2 (hm : m ≤ m0) (f : α →₂[μ] E) :
    AEStronglyMeasurable[m] (condExpL2 E 𝕜 hm f : α → E) μ :=
  lpMeas.aestronglyMeasurable _

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