toOuterMeasure_apply_finset — Mathlib

English

For a finite index set s, p.toOuterMeasure(s) equals the finite sum of p(x) over x in s.

Русский

Для конечного множества s верно p.toOuterMeasure(s) = сумма p(x) по x ∈ s.

LaTeX

$$$ p.toOuterMeasure(s) = \sum_{x \in s} p(x) $$$

Lean4

@[simp]
theorem toOuterMeasure_apply_finset (s : Finset α) : p.toOuterMeasure s = ∑ x ∈ s, p x :=
  by
  refine (toOuterMeasure_apply p s).trans ((tsum_eq_sum (s := s) ?_).trans ?_)
  · exact fun x hx => Set.indicator_of_notMem (Finset.mem_coe.not.2 hx) _
  · exact Finset.sum_congr rfl fun x hx => Set.indicator_of_mem (Finset.mem_coe.2 hx) _

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