English
The measure defined from a sigma-subadditive content on a semiring agrees with the content on the semiring.
Русский
Мера, заданная через сигма-субаддитивное содержимое на полуребре, согласуется с содержимым на полуребре.
LaTeX
$$$m.measure hC hC\\_gen.le m\\_sigma\\_subadd s = m s \\quad (s \\in C).$$$
Lean4
/-- The measure defined through a sigma-subadditive
content on a semiring coincides with the content on the semiring. -/
theorem measure_eq [mα : MeasurableSpace α] (m : AddContent C) (hC : IsSetSemiring C)
(hC_gen : mα = MeasurableSpace.generateFrom C) (m_sigma_subadd : m.IsSigmaSubadditive) (hs : s ∈ C) :
m.measure hC hC_gen.le m_sigma_subadd s = m s :=
by
rw [measure, trim_measurableSet_eq]
· exact m.measureCaratheodory_eq hC m_sigma_subadd hs
· rw [hC_gen]
apply MeasurableSpace.measurableSet_generateFrom hs
