comp_aestronglyMeasurable — Mathlib

English

If f is continuous and the relevant second-countability condition holds, then f is AEStronglyMeasurable.

Русский

Если функция непрерывна и выполняется условие второго счётного базиса, то она AE‑строго измерима.

LaTeX

$$$\\text{Continuous}(f) \\Rightarrow AEStronglyMeasurable(f, \\mu)$ under appropriate second countability$$

Lean4

/-- The composition of a continuous function and an ae strongly measurable function is ae strongly
measurable. -/
@[fun_prop]
theorem _root_.Continuous.comp_aestronglyMeasurable {g : β → γ} {f : α → β} (hg : Continuous g)
    (hf : AEStronglyMeasurable[m] f μ) : AEStronglyMeasurable[m] (fun x => g (f x)) μ :=
  ⟨_, hg.comp_stronglyMeasurable hf.stronglyMeasurable_mk, EventuallyEq.fun_comp hf.ae_eq_mk g⟩

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