English
Under equality of underlying measurable structure with generatedFrom C, the measure from AddContent coincides with m on C.
Русский
При равенстве порождающей сигма-алгебры и заданной структуры измеримости мера от AddContent совпадает с m на C.
LaTeX
$$$m.measure hC hC\\_gen.le m\\_sigma\\_subadd s = m s\\quad (s \\in C).$$$
Lean4
/-- Construct a measure from a sigma-subadditive content on a semiring, assuming the semiring
generates a given measurable structure. The measure is defined on this measurable structure. -/
noncomputable def measure [mα : MeasurableSpace α] (m : AddContent C) (hC : IsSetSemiring C)
(hC_gen : mα ≤ MeasurableSpace.generateFrom C) (m_sigma_subadd : m.IsSigmaSubadditive) : Measure α :=
(m.measureCaratheodory hC m_sigma_subadd).trim <| fun s a ↦ isCaratheodory_inducedOuterMeasure hC m s (hC_gen s a)
