sum_measure_singleton — Mathlib

English

For a Finset s of α and a MeasurableSingletonClass, ∑ x ∈ s μ({x}) = μ(s).

Русский

Пусть s — конечное множество подмножеств; мера одного элемента μ({x}) суммируется по всем x ∈ s и равна мере множества s.

LaTeX

$$$$ \\sum_{x \\in s} \\mu\\{x\\} = \\mu(s). $$$$

Lean4

@[simp]
theorem sum_measure_singleton {s : Finset α} [MeasurableSingletonClass α] : ∑ x ∈ s, μ { x } = μ s :=
  by
  trans ∑ x ∈ s, μ (id ⁻¹' { x })
  · simp
  rw [sum_measure_preimage_singleton]
  · simp
  · simp

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