summable_measure_toReal — Mathlib

English

If μ is finite and f_i are measurable with pairwise disjoint f_i, then the sequence x ↦ μ.real(f_x) is summable.

Русский

Если μ конечна и f_i измеримы и пары f_i взаимно непересекаются, то последовательность x ↦ μ.real(f_x) образует суммируемость.

LaTeX

$$$(\forall i, \text{MeasurableSet}(f_i)) \land \text{Pairwise}(\text{Disjoint on } f) \Rightarrow \operatorname{Summable}(i \mapsto \mu.\mathrm{real}(f_i))$$

Lean4

theorem summable_measure_toReal [hμ : IsFiniteMeasure μ] {f : ℕ → Set α} (hf₁ : ∀ i : ℕ, MeasurableSet (f i))
    (hf₂ : Pairwise (Disjoint on f)) : Summable fun x => μ.real (f x) :=
  by
  apply ENNReal.summable_toReal
  rw [← MeasureTheory.measure_iUnion hf₂ hf₁]
  exact ne_of_lt (measure_lt_top _ _)

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