lintegral_lt_top_of_nnreal — Mathlib

English

For a finite measure μ and a bounded continuous f: X → NNReal, the lintegral of f is strictly below the top element of ENNReal.

Русский

При конечной мере μ и ограниченной непрерывной f: X → NNReal линегральный интеграл строго меньше максимального элемента ENNReal.

LaTeX

$$$$\\int^{ - } x, f(x) ∂\\mu < \\infty.$$$$

Lean4

theorem lintegral_lt_top_of_nnreal (f : X →ᵇ ℝ≥0) : ∫⁻ x, f x ∂μ < ∞ :=
  by
  apply IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal
  refine ⟨nndist f 0, fun x ↦ ?_⟩
  have key := BoundedContinuousFunction.NNReal.upper_bound f x
  rwa [ENNReal.coe_le_coe]

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