toOuterMeasure_apply_fintype — Mathlib

English

If the intersections with the support are equal, the outer measures are equal.

Русский

Если пересечения с опорой равны, внешние меры равны.

LaTeX

$$$ p.toOuterMeasure s = p.toOuterMeasure t \iff s \cap \mathrm{supp}(p) = t \cap \mathrm{supp}(p) $$$

Lean4

@[simp]
theorem toOuterMeasure_apply_fintype [Fintype α] : p.toOuterMeasure s = ∑ x, s.indicator p x :=
  (p.toOuterMeasure_apply s).trans (tsum_eq_sum fun x h => absurd (Finset.mem_univ x) h)

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