restrict_apply' — Mathlib

English

If s is measurable, then μ|s(t) = μ(t ∩ s) for all t.

Русский

Если s измеримо, то для всех t имеет место μ|s(t) = μ(t ∩ s).

LaTeX

$$$\text{restrict applied on measurable } s: \ μ|s(t) = μ(t \cap s).$$$

Lean4

/-- If `s` is a measurable set, then the outer measure of `t` with respect to the restriction of
the measure to `s` equals the outer measure of `t ∩ s`. This is an alternate version of
`Measure.restrict_apply`, requiring that `s` is measurable instead of `t`. -/
@[simp]
theorem restrict_apply' (hs : MeasurableSet s) : μ.restrict s t = μ (t ∩ s) := by
  rw [← toOuterMeasure_apply, Measure.restrict_toOuterMeasure_eq_toOuterMeasure_restrict hs,
    OuterMeasure.restrict_apply s t _, toOuterMeasure_apply]

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