aemeasurable — Mathlib

English

A strongly measurable function is almost everywhere measurable with respect to any measure μ.

Русский

Сильно измеримая функция является почти всюду измеримой относительно любой меры μ.

LaTeX

$$$\text{StronglyMeasurable}(f) \Rightarrow \mathrm{AEMeasurable}(f,\mu)$$$

Lean4

/-- A strongly measurable function is almost everywhere measurable. -/
@[aesop 5% apply (rule_sets := [Measurable])]
protected theorem aemeasurable {_ : MeasurableSpace α} [TopologicalSpace β] [PseudoMetrizableSpace β]
    [MeasurableSpace β] [BorelSpace β] {μ : Measure α} (hf : StronglyMeasurable f) : AEMeasurable f μ :=
  hf.measurable.aemeasurable

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