measure_eq_top_of_lintegral_ne_top

English

If the lintegral ∫ f dμ is not ∞, then μ({x | f x = ∞}) = 0.

Русский

Если линеграл не равен бесконечности, то мера множества бесконечных значений f(x) равна нулю.

LaTeX

$$$$ \mu\{x \mid f(x)=\infty\} = 0. $$$$

Lean4

theorem measure_eq_top_of_lintegral_ne_top {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hμf : ∫⁻ x, f x ∂μ ≠ ∞) :
    μ {x | f x = ∞} = 0 :=
  of_not_not fun h => hμf <| lintegral_eq_top_of_measure_eq_top_ne_zero hf h

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