finStronglyMeasurable_of_measurable

English

In a second-countable space with sigma-finite measure, a measurable function is Finite Strongly Measurable.

Русский

Во втором счетном пространстве с сигма-ограниченной мерой измеримая функция является финитно сильно измеримой.

LaTeX

$$$\text{Measurable}(f) \Rightarrow \text{FinStronglyMeasurable}(f,\mu)$$$

Lean4

/-- In a space with second countable topology and a sigma-finite measure, a measurable function
is `FinStronglyMeasurable`. -/
@[aesop 90% apply (rule_sets := [Measurable])]
theorem finStronglyMeasurable_of_measurable {_m0 : MeasurableSpace α} (μ : Measure α) [SigmaFinite μ]
    (hf : Measurable f) : FinStronglyMeasurable f μ :=
  (finStronglyMeasurable_iff_measurable μ).mpr hf

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