setLIntegral_const_lt_top — Mathlib

English

For a finite measure μ and a finite constant c ≠ ∞, the integral of the constant function c over any set s is finite.

Русский

Пусть μ является конечной мерой, а константа c конечна; интеграл константы c по любому множеству s конечен.

LaTeX

$$$$\\int_{a\\in s} c \\, d\\mu < \\infty.$$$$

Lean4

theorem setLIntegral_const_lt_top [IsFiniteMeasure μ] (s : Set α) {c : ℝ≥0∞} (hc : c ≠ ∞) : ∫⁻ _ in s, c ∂μ < ∞ :=
  by
  rw [lintegral_const]
  exact ENNReal.mul_lt_top hc.lt_top (measure_lt_top (μ.restrict s) univ)

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