measureCaratheodory_eq_inducedOuterMeasure

English

The measureCaratheodory constructed from AddContent m coincides with the inducedOuterMeasure.

Русский

Мера, полученная через measureCaratheodory от AddContent m, совпадает с inducedOuterMeasure.

LaTeX

$$$m\\_measure \\; hC\\; m\\_sigma\\_subadd = m\\_inducedOuterMeasure.$$$

Lean4

/-- The measure `MeasureTheory.AddContent.measureCaratheodory` generated from an
`m : AddContent C` on a `IsSetSemiring C` coincides with the `MeasureTheory.inducedOuterMeasure`. -/
theorem measureCaratheodory_eq_inducedOuterMeasure (hC : IsSetSemiring C) (m : AddContent C)
    (m_sigma_subadd : m.IsSigmaSubadditive) :
    m.measureCaratheodory hC m_sigma_subadd s = inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty s :=
  rfl

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