sum_measure_preimage_singleton — Mathlib

English

Let f be a simple function α → β and μ a measure on α. For any finite set s ⊆ β, the sum over y in s of μ(f^{-1}({y})) equals μ(f^{-1}(↑s)).

Русский

Пусть f : α → β — простая функция и μ — мера на α. Для любого конечного множества s ⊆ β сумма по y ∈ s μ(f^{-1}({y})) равна μ(f^{-1}(↑s)).

LaTeX

$$$\\displaystyle \\sum_{y \\in s} \\mu\\big(f^{-1}(\\{y\\})\\big) = \\mu\\big(f^{-1}(\\uparrow s)\\big)$$$

Lean4

protected theorem sum_measure_preimage_singleton (f : α →ₛ β) {μ : Measure α} (s : Finset β) :
    (∑ y ∈ s, μ (f ⁻¹' { y })) = μ (f ⁻¹' ↑s) :=
  sum_measure_preimage_singleton _ fun _ _ => f.measurableSet_fiber _

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