finStronglyMeasurable — Mathlib

English

If μ is sigma-finite, every strongly measurable function is Finite-strongly measurable with respect to μ.

Русский

Если μ сигма-ограничена, каждая сильно измеримая функция является финитно-сильно измеримой относительно μ.

LaTeX

$$$\SigmaFinite(\mu) \Rightarrow \mathrm{FinStronglyMeasurable}(f,\mu)\quad\text{for } f \text{ strongly measurable}$$$

Lean4

/-- If the measure is sigma-finite, all strongly measurable functions are
  `FinStronglyMeasurable`. -/
@[aesop 5% apply (rule_sets := [Measurable])]
protected theorem finStronglyMeasurable [TopologicalSpace β] [Zero β] {m0 : MeasurableSpace α}
    (hf : StronglyMeasurable f) (μ : Measure α) [SigmaFinite μ] : FinStronglyMeasurable f μ :=
  hf.finStronglyMeasurable_of_set_sigmaFinite MeasurableSet.univ (by simp) (by rwa [Measure.restrict_univ])

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