English
If s is measurable with respect to the sigma-algebra generated by C, then the induced outer measure from AddContent m is Carathéodory-measurable on s.
Русский
Если s измеримо относительно сигма-алгебры, порождённой C, то индуцированная внешняя мера от содержимого добавляет Карпатодорову измеримость на s.
LaTeX
$$$\\text{If } \\text{MeasurableSet}_{\\text{generateFrom}(C)}(s)\\;\\text{ then } (inducedOuterMeasure (fun x \\to m x) hC.empty_mem addContent_empty).IsCaratheodory\\; s.$$$
Lean4
theorem isCaratheodory_inducedOuterMeasure (hC : IsSetSemiring C) (m : AddContent C) (s : Set α)
(hs : MeasurableSet[MeasurableSpace.generateFrom C] s) :
(inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty).IsCaratheodory s := by
induction hs with
| basic u hu => exact isCaratheodory_inducedOuterMeasure_of_mem hC m hu
| empty => exact OuterMeasure.isCaratheodory_empty _
| compl t _ h => exact OuterMeasure.isCaratheodory_compl _ h
| iUnion f _ h => exact OuterMeasure.isCaratheodory_iUnion _ h
