toMeasure_mono — Mathlib

English

If s is measurable and s ∩ p.support ⊆ t, then p.toMeasure s ≤ p.toMeasure t.

Русский

Если s измеримо и s ∩ опора(p) ⊆ t, то p.toMeasure s ≤ p.toMeasure t.

LaTeX

$$$ p.toMeasure s \le p.toMeasure t $ given $ s \cap p.support ⊆ t $ and MeasurableSet s.$$

Lean4

theorem toMeasure_mono {t : Set α} (hs : MeasurableSet s) (h : s ∩ p.support ⊆ t) : p.toMeasure s ≤ p.toMeasure t :=
  by
  rw [p.toMeasure_apply_eq_toOuterMeasure_apply hs]
  exact (p.toOuterMeasure_mono h).trans (p.toOuterMeasure_apply_le_toMeasure_apply t)

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