toOuterMeasure_ofFinset_apply — Mathlib

English

The outer measure of the PMF built from a Finset is given by the sum over the indicator of f on t.

Русский

Внешняя мера PMF, построенного из Finset, задаётся суммой по индикатору f на t.

LaTeX

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

Lean4

@[simp]
theorem toOuterMeasure_ofFinset_apply : (ofFinset f s h h').toOuterMeasure t = ∑' x, t.indicator f x :=
  toOuterMeasure_apply (ofFinset f s h h') t

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