sum_range_measure_preimage_singleton

English

Let f be a simple function α → β and μ a measure on α. Then the sum over all y in the range of f of μ(f^{-1}({y})) equals μ(univ).

Русский

Пусть f : α → β — простая функция и μ — мера на α. Тогда сумма по всем y из диапазона f μ(f^{-1}({y})) равна μ(всё пространство).

LaTeX

$$$\\displaystyle \\sum_{y \\in f.range} \\mu\\big(f^{-1}(\\{y\\})\\big) = \\mu(\\mathrm{univ})$$$

Lean4

theorem sum_range_measure_preimage_singleton (f : α →ₛ β) (μ : Measure α) : (∑ y ∈ f.range, μ (f ⁻¹' { y })) = μ univ :=
  by rw [f.sum_measure_preimage_singleton, coe_range, preimage_range]

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