toMeasure_ofFintype_apply — Mathlib

English

For a measurable α and finite type, the toMeasure of the PMF from Fintype equals the sum of s.indicator f.

Русский

Для измеримого множества α и конечного типа сумма по s.indicator f описывает toMeasure PMF.

LaTeX

$$$ (toMeasure (ofFintype f h)) s = \sum' x, s.indicator f x $$$$

Lean4

@[simp]
theorem toMeasure_ofFintype_apply [MeasurableSpace α] (hs : MeasurableSet s) :
    (ofFintype f h).toMeasure s = ∑' x, s.indicator f x :=
  (toMeasure_apply_eq_toOuterMeasure_apply _ hs).trans (toOuterMeasure_ofFintype_apply h s)

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