lintegral_lt_top_of_bounded_to_ennreal

English

For a finite measure μ, if f is bounded by some NNReal, then the lintegral of f is finite.

Русский

Для конечной меры μ, если f ограничена некоторым NNReal, то линегральный интеграл конечен.

LaTeX

$$$$\\int f \\partial\\mu < \\infty.$$$$

Lean4

theorem _root_.IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal [IsFiniteMeasure μ] {f : α → ℝ≥0∞}
    (f_bdd : ∃ c : ℝ≥0, ∀ x, f x ≤ c) : ∫⁻ x, f x ∂μ < ∞ :=
  by
  rw [← μ.restrict_univ]
  refine setLIntegral_lt_top_of_le_nnreal (measure_ne_top _ _) ?_
  simpa using f_bdd

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