setLIntegral_lt_top_of_isCompact — Mathlib

English

If the space α has a compact measurable set s and f is continuous, then the lintegral of f over s is finite provided μ(s) is finite.

Русский

Если множество s компактно и измеримо, и f непрерывна, то линегральный интеграл по s конечен при конечной мере μ(s).

LaTeX

$$$$\\int_{a\\in s} f(a) \\, d\\mu < \\infty.$$$$

Lean4

theorem setLIntegral_lt_top_of_isCompact [TopologicalSpace α] {s : Set α} (hs : μ s ≠ ∞) (hsc : IsCompact s)
    {f : α → ℝ≥0} (hf : Continuous f) : ∫⁻ x in s, f x ∂μ < ∞ :=
  setLIntegral_lt_top_of_bddAbove hs (hsc.image hf).bddAbove

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