inducedOuterMeasure_eq — Mathlib

English

Under the same hypotheses, the induced outer measure agrees with the original outer measure on measurable sets: for every measurable s, the inducedOuterMeasure m equalizes with m on s.

Русский

При тех же предпосылках индуцированная внешняя мера совпадает с исходной внешней мерой на измеримых множествах: для каждого измеримого s имеет место равенство между индуцированной и исходной мерой на s.

LaTeX

$$$\\forall s \, (MeasurableSet(s) \\Rightarrow \\ operatorname{inducedOuterMeasure} (m) \\; s = m \\; s \\; s)$$$

Lean4

theorem inducedOuterMeasure_eq {s : Set α} (hs : MeasurableSet s) :
    inducedOuterMeasure m MeasurableSet.empty m0 s = m s hs :=
  (inducedOuterMeasure_eq_extend m0 mU hs).trans <| extend_eq _ _

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