isCaratheodory_inducedOuterMeasure_of_mem

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

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