aestronglyMeasurable — Mathlib

English

In a space with a suitable second-countable topology, measurable functions are AEStronglyMeasurable.

Русский

В пространстве с подходящей второй счетной топологией измеримые функции являются AEStronglyMeasurable.

LaTeX

$$$\text{Measurable}(f) \rightarrow AEStronglyMeasurable\, f\ μ$$$

Lean4

/-- In a space with second countable topology, measurable implies ae strongly measurable. -/
@[fun_prop, aesop unsafe 30% apply (rule_sets := [Measurable])]
theorem _root_.Measurable.aestronglyMeasurable [MeasurableSpace β] [PseudoMetrizableSpace β] [SecondCountableTopology β]
    [OpensMeasurableSpace β] (hf : Measurable[m] f) : AEStronglyMeasurable[m] f μ :=
  hf.stronglyMeasurable.aestronglyMeasurable

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