lintegral_lt_top — Mathlib

English

If f: α → ℝ is integrable with respect to μ, then the Lintegral of f (via the nonnegative real extension) is finite; in particular ∫ |f| dμ < ∞.

Русский

Пусть f: α → ℝ интегрируема по μ. Тогда линегральная интеграл(f) конечен, то есть ∫ |f| dμ < ∞.

LaTeX

$$$\\text{If } f: \\alpha \\to \\mathbb{R} \\text{ is integrable w.r.t. } \\mu, \\\\ \\int^{-}_{x} \\! \\mathrm{ENNReal.ofReal}(f(x)) \\, d\\mu \; < \\; \\infty.$$$

Lean4

theorem lintegral_lt_top {f : α → ℝ} (hf : Integrable f μ) : (∫⁻ x, ENNReal.ofReal (f x) ∂μ) < ∞ :=
  calc
    (∫⁻ x, ENNReal.ofReal (f x) ∂μ) ≤ ∫⁻ x, ↑‖f x‖₊ ∂μ := lintegral_ofReal_le_lintegral_enorm f
    _ < ∞ := hf.2

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