toMeasure_ofFinset_apply — Mathlib

English

The toMeasure of the PMF built from Finset, for a set t, equals the sum of t.indicator f.

Русский

ToMeasure PMF, построенного через Finset, на множество t равна сумме t.indicator f.

LaTeX

$$$ (toMeasure (ofFinset f s h h')) t = ∑' x, t.indicator f x $$$

Lean4

@[simp]
theorem toMeasure_ofFinset_apply [MeasurableSpace α] (ht : MeasurableSet t) :
    (ofFinset f s h h').toMeasure t = ∑' x, t.indicator f x :=
  (toMeasure_apply_eq_toOuterMeasure_apply _ ht).trans (toOuterMeasure_ofFinset_apply h h' t)

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