toOuterMeasure_mono — Mathlib

English

If s and t agree on their intersection with the support of p, then p.toOuterMeasure(s) = p.toOuterMeasure(t).

Русский

Если s и t совпадают на своей пересечении с опорой p, то p.toOuterMeasure(s) = p.toOuterMeasure(t).

LaTeX

$$$ p.toOuterMeasure s = p.toOuterMeasure t \;\text{ если } s \cap \mathrm{supp}(p) = t \cap \mathrm{supp}(p). $$$

Lean4

/-- Slightly stronger than `OuterMeasure.mono` having an intersection with `p.support`. -/
theorem toOuterMeasure_mono {s t : Set α} (h : s ∩ p.support ⊆ t) : p.toOuterMeasure s ≤ p.toOuterMeasure t :=
  le_trans (le_of_eq (toOuterMeasure_apply_inter_support p s).symm) (p.toOuterMeasure.mono h)

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