aefinStronglyMeasurable_of_aemeasurable

English

In a second-countable, sigma-finite setting, AEFinStronglyMeasurable is equivalent to AEMeasurable.

Русский

В условиях вторичного счётного пространства и сигма-конечной меры AEFinStronglyMeasurable эквивалентна AEMeasurable.

LaTeX

$$$\\text{AEFinStronglyMeasurable}(f,\\mu) \\iff \\text{AEMeasurable}(f,\\mu)$$$

Lean4

/-- In a space with second countable topology and a sigma-finite measure,
  an `AEMeasurable` function is `AEFinStronglyMeasurable`. -/
@[aesop 90% apply (rule_sets := [Measurable])]
theorem aefinStronglyMeasurable_of_aemeasurable {_m0 : MeasurableSpace α} (μ : Measure α) [SigmaFinite μ]
    (hf : AEMeasurable f μ) : AEFinStronglyMeasurable f μ :=
  (aefinStronglyMeasurable_iff_aemeasurable μ).mpr hf

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