aestronglyMeasurable_iff_aemeasurable

English

In spaces with a second countable topology and Borel structure, strong measurability and almost-everywhere measurability coincide: AEStronglyMeasurable f μ is equivalent to AEMeasurable f μ.

Русский

В пространствах со второй счетной топологией и борелевой структурой сильная измеримость и измеримость почти всюду эквивалентны: AEStronglyMeasurable f μ эквивалентно AEMeasurable f μ.

LaTeX

$$$AEStronglyMeasurable(f, \mu) \iff AEMeasurable(f, \mu)$$$

Lean4

/-- In a space with second countable topology, strongly measurable and measurable are equivalent. -/
theorem _root_.aestronglyMeasurable_iff_aemeasurable [PseudoMetrizableSpace β] [BorelSpace β]
    [SecondCountableTopology β] : AEStronglyMeasurable f μ ↔ AEMeasurable f μ :=
  ⟨fun h => h.aemeasurable, fun h => h.aestronglyMeasurable⟩

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