lintegral_const_lt_top — Mathlib

English

If μ is a probability measure and f equals a constant c almost everywhere, then the lintegral of f equals c.

Русский

Если μ является вероятностной мерой и f равно константе c почти всюду, то линегральный интеграл равен c.

LaTeX

$$$$\\int f \\, d\\mu = c \\quad\\text{if } f = c \\text{ a.e. } \\mu.$$$$

Lean4

theorem lintegral_const_lt_top [IsFiniteMeasure μ] {c : ℝ≥0∞} (hc : c ≠ ∞) : ∫⁻ _, c ∂μ < ∞ := by
  simpa only [Measure.restrict_univ] using setLIntegral_const_lt_top (univ : Set α) hc

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