sum_measureReal_singleton — Mathlib

English

If β is finite, then μ.real (⋃ b, f(b)) ≤ ∑ p, μ.real (f p).

Русский

Если β конечен, то μ.real(⋃_{b} f(b)) ≤ ∑_{p} μ.real(f(p)).

LaTeX

$$$ \\mu.real (\\bigcup_{b} f(b)) \\leq \\sum_{p} \\mu.real (f(p)) $$$

Lean4

/-- If `s` is a `Finset`, then the sums of the real measures of the singletons in the set is the
real measure of the set. -/
@[simp]
theorem sum_measureReal_singleton [MeasurableSingletonClass α] [SigmaFinite μ] (s : Finset α) :
    (∑ b ∈ s, μ.real { b }) = μ.real s := by
  simp [measureReal_def, ← ENNReal.toReal_sum (fun _ _ ↦ ne_of_lt measure_singleton_lt_top)]

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