toMeasure_apply_fintype — Mathlib

English

If α is finite, then p.toMeasure s equals the finite sum over all x of s.indicator(p x).

Русский

Если множество α конечно, то p.toMeasure s равно конечной сумме по всем x: s.indicator(p x).

LaTeX

$$$\\forall s:\\ Set(\\alpha),\\ [\\text{Fintype }\\alpha] \\\\; p.toMeasure s = \\sum x, s.indicator(p x)$$$

Lean4

@[simp]
theorem toMeasure_apply_fintype (s : Set α) [Fintype α] : p.toMeasure s = ∑ x, s.indicator p x :=
  (p.toMeasure_apply_eq_toOuterMeasure s).trans (p.toOuterMeasure_apply_fintype s)

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