ofReal_setIntegral_one — Mathlib

English

For a finite measure μ on X and a set s, ENNReal.ofReal (∫_{x∈s} 1 dμ) = μ(s).

Русский

Для конечной меры μ на X и множества s верно: ENNReal.ofReal (∫_{x∈s} 1 dμ) = μ(s).

LaTeX

$$$$ \operatorname{ENNReal.ofReal}\left( \int_{x\in s} 1 \, d\mu \right) = \mu(s). $$$$

Lean4

theorem ofReal_setIntegral_one {X : Type*} {_ : MeasurableSpace X} (μ : Measure X) [IsFiniteMeasure μ] (s : Set X) :
    ENNReal.ofReal (∫ _ in s, (1 : ℝ) ∂μ) = μ s :=
  ofReal_setIntegral_one_of_measure_ne_top

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