English
Every set in C is Carathéodory-measurable with respect to the induced outer measure coming from AddContent m extended to m.extend hC.
Русский
Каждое множество из C является Карпатодоревой измеримой относительно индуцированной внешней меры, полученной из AddContent m и его продолжения.
LaTeX
$$$\\text{For } hs: s \\in C,\\; (inducedOuterMeasure (fun x \\to m x) hC.empty_mem addContent_empty)\\ IsCaratheodory\\; s.$$$
Lean4
/-- Every `s ∈ C` for an `m : AddContent C` with `IsSetSemiring C` is Carathéodory measurable
with respect to the `inducedOuterMeasure` from `m`. -/
theorem isCaratheodory_inducedOuterMeasure_of_mem (hC : IsSetSemiring C) (m : AddContent C) {s : Set α} (hs : s ∈ C) :
(inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty).IsCaratheodory s :=
isCaratheodory_ofFunction_of_mem hC (m.extend hC) (fun _ ↦ m.extend_eq_top hC) hs