toMeasure_apply_eq_of_inter_support_eq

English

If s and t are measurable sets and their intersections with the support of p coincide, then p.toMeasure(s) = p.toMeasure(t).

Русский

Если s и t — измеримые множества, и их пересечения с опорой p совпадают, то p.toMeasure(s) = p.toMeasure(t).

LaTeX

$$$\\forall s,t\\; (hs : MeasurableSet\, s) (ht : MeasurableSet\, t)\\; (h:\\, s \\cap \\operatorname{supp}(p) = t \\cap \\operatorname{supp}(p))\\; \\, \\Rightarrow\\; p.toMeasure(s) = p.toMeasure(t)$$$

Lean4

theorem toMeasure_apply_eq_of_inter_support_eq {t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t)
    (h : s ∩ p.support = t ∩ p.support) : p.toMeasure s = p.toMeasure t := by
  simpa only [p.toMeasure_apply_eq_toOuterMeasure_apply, hs, ht] using p.toOuterMeasure_apply_eq_of_inter_support_eq h

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