aefinStronglyMeasurable_iff_aemeasurable

English

The same as above, sigmaFiniteSet defines a witness t for sigma-finiteness and a.e. zero outside.

Русский

То же самое: sigmaFiniteSet определяет множество свидетель для сигма-конечности и нулевые значения вне него.

LaTeX

$$$\\sigmaFiniteSet(f)$ является наблюдаемым множеством и обеспечивает $f =^{\\mathrm{a}}_{\\mu|_{\\sigmaFiniteSet(f)^c}} 0$ и $\\Sigma$Finite$(\\mu|_{\\sigmaFiniteSet(f)})$$$

Lean4

/-- In a space with second countable topology and a sigma-finite measure,
  `AEFinStronglyMeasurable` and `AEMeasurable` are equivalent. -/
theorem aefinStronglyMeasurable_iff_aemeasurable {_m0 : MeasurableSpace α} (μ : Measure α) [SigmaFinite μ] :
    AEFinStronglyMeasurable f μ ↔ AEMeasurable f μ := by
  simp_rw [AEFinStronglyMeasurable, AEMeasurable, finStronglyMeasurable_iff_measurable]

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