aestronglyMeasurable — Mathlib

English

If a function f is almost everywhere measurable with respect to a measure μ, then it is almost everywhere strongly measurable with respect to μ (in spaces with the standard second-countable topology assumptions).

Русский

Если функция f почти всюду измерима по мере μ, то она почти всюду сильно измерима по μ (в пространствах с обычной теоремой второго счетчика).

LaTeX

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

Lean4

/-- In a space with second countable topology, measurable implies strongly measurable. -/
@[fun_prop, aesop 90% apply (rule_sets := [Measurable])]
theorem _root_.AEMeasurable.aestronglyMeasurable [PseudoMetrizableSpace β] [OpensMeasurableSpace β]
    [SecondCountableTopology β] (hf : AEMeasurable f μ) : AEStronglyMeasurable f μ :=
  ⟨hf.mk f, hf.measurable_mk.stronglyMeasurable, hf.ae_eq_mk⟩

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