toOuterMeasure_ofFintype_apply — Mathlib

English

The toOuterMeasure of the PMF from a finite type corresponds to summing the indicator of f over the set.

Русский

ToOuterMeasure PMF из конечного типа соответствует суммированию индикатора f по множеству.

LaTeX

$$$ toOuterMeasure_ofFintype_apply : (ofFintype f h).toOuterMeasure s = ∑' x, s.indicator f x $$$

Lean4

@[simp high]
theorem toOuterMeasure_ofFintype_apply : (ofFintype f h).toOuterMeasure s = ∑' x, s.indicator f x :=
  toOuterMeasure_apply (ofFintype f h) s

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