English
Let m be a family of set-valued outer-measure assignments on a measurable space with m(∅) = 0 and a σ-additivity-type property for disjoint countable unions. Then the outer measure induced by m coincides with the canonical extension on all measurable sets: for every measurable s, the inducedOuterMeasure m equals extend m on s.
Русский
Пусть m — семейство наружных мер, заданное на измеримом пространстве, удовлетворяющее условию m(∅) = 0 и аналогичному свойству суммирования по попарно непересекающимся счётным объединениям. Тогда индуцированная внешняя мера совпадает с каноническим расширением на всех измеримых множествах: для любого измеримого s имеет место равенство ind m s = extend m s.
LaTeX
$$$\\forall s \, (MeasurableSet(s) \,\\Rightarrow \\ inducedOuterMeasure\\; m\\; MeasurableSet.empty \\; m0\\; s) = \\ operatorname{extend} (m) \\; s$$$
Lean4
theorem inducedOuterMeasure_eq_extend {s : Set α} (hs : MeasurableSet s) :
inducedOuterMeasure m MeasurableSet.empty m0 s = extend m s :=
ofFunction_eq s (fun _t => extend_mono m0 mU hs) (extend_iUnion_le_tsum_nat m0 mU)
