toOuterMeasure_apply_eq_of_inter_support_eq

English

For any p and s,t with the same intersection with p.support, the corresponding outer measures are equal.

Русский

Для любого p и s,t с равными пересечениями с опорой p соответствующие внешние меры равны.

LaTeX

$$$ \forall p: PMF(\alpha),\ s,t: Set(\alpha),\ s\cap p.{\n}support = t\cap p.{\n}support \Rightarrow p.toOuterMeasure s = p.toOuterMeasure t $$$

Lean4

theorem toOuterMeasure_apply_eq_of_inter_support_eq {s t : Set α} (h : s ∩ p.support = t ∩ p.support) :
    p.toOuterMeasure s = p.toOuterMeasure t :=
  le_antisymm (p.toOuterMeasure_mono (h.symm ▸ Set.inter_subset_left))
    (p.toOuterMeasure_mono (h ▸ Set.inter_subset_left))

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