setIntegral_one_eq_measureReal — Mathlib

English

For any set s, the integral of the constant function 1 over s equals the real-valued measure of s, μ.real(s).

Русский

Для множества s интеграл константы 1 по s равен вещественной мере μ.real(s).

LaTeX

$$$$ \int_{x \in s} 1 \, d\mu = \mu.{real}(s) $$$$

Lean4

theorem setIntegral_one_eq_measureReal {X : Type*} {m : MeasurableSpace X} {μ : Measure X} {s : Set X} :
    ∫ _ in s, (1 : ℝ) ∂μ = μ.real s := by simp

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