aestronglyMeasurable — Mathlib

English

Locally integrable implies that f is AEStronglyMeasurable under appropriate separability/metric assumptions.

Русский

Локальная интегрируемость подразумевает AEStronglyMeasurable при заданных условиях разделимости/метричности.

LaTeX

$$$\\operatorname{LocallyIntegrable} f\\mu \\Rightarrow \\operatorname{AEStronglyMeasurable} f\\mu$$$

Lean4

theorem aestronglyMeasurable [PseudoMetrizableSpace ε] [SecondCountableTopology X] (hf : LocallyIntegrable f μ) :
    AEStronglyMeasurable f μ := by
  simpa only [restrict_univ] using (locallyIntegrableOn_univ.mpr hf).aestronglyMeasurable

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