sum_measure_preimage_singleton — Mathlib

English

For s a Finset of β and f: α → β with ∀ y ∈ s, MeasurableSet (f^{-1}{y}), we have ∑ b ∈ s μ(f^{-1}{b}) = μ(f^{-1} s).

Русский

Пусть s — конечное множество индексов β и для каждого b ∈ s множество f^{-1}{b} измеримо; тогда сумма мер этих предобразов равна мере предобраза множества s.

LaTeX

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

Lean4

/-- If `s` is a `Finset`, then the measure of its preimage can be found as the sum of measures
of the fibers `f ⁻¹' {y}`. -/
theorem sum_measure_preimage_singleton (s : Finset β) {f : α → β} (hf : ∀ y ∈ s, MeasurableSet (f ⁻¹' { y })) :
    (∑ b ∈ s, μ (f ⁻¹' { b })) = μ (f ⁻¹' ↑s) := by
  simp only [← measure_biUnion_finset (pairwiseDisjoint_fiber f s) hf, Finset.set_biUnion_preimage_singleton]

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