tsum_measure_preimage_singleton — Mathlib

English

If s is countable, then the measure of the preimage of s under f is the sum over s of the measures of the singletons preimages.

Русский

Если множество s счетно, то мера объединения предобраза множества s равна сумме мер предобразов каждого элемента.

LaTeX

$$$$ \\sum_{b \\in s} \\mu\\left(f^{-1}\\{\\uparrow b\\}\\right) = \\mu\\left(f^{-1}[s]\\right). $$$$

Lean4

/-- If `s` is a countable set, then the measure of its preimage can be found as the sum of measures
of the fibers `f ⁻¹' {y}`. -/
theorem tsum_measure_preimage_singleton {s : Set β} (hs : s.Countable) {f : α → β}
    (hf : ∀ y ∈ s, MeasurableSet (f ⁻¹' { y })) : (∑' b : s, μ (f ⁻¹' {↑b})) = μ (f ⁻¹' s) := by
  rw [← Set.biUnion_preimage_singleton, measure_biUnion hs (pairwiseDisjoint_fiber f s) hf]

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