aemeasurable — Mathlib

English

If f is integrable with respect to μ, then f is almost everywhere measurable (AEMeasurable) with respect to μ.

Русский

Если f интегрируема по μ, то она является почти сигнально измеримой (AEMeasurable) по μ.

LaTeX

$$$\operatorname{Integrable}(f, \mu) \Rightarrow \operatorname{AEMeasurable}(f, \mu)$$$

Lean4

@[fun_prop]
theorem aemeasurable [MeasurableSpace ε] [BorelSpace ε] [PseudoMetrizableSpace ε] {f : α → ε} (hf : Integrable f μ) :
    AEMeasurable f μ :=
  hf.aestronglyMeasurable.aemeasurable

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