Hi,
> I have a question about the new version of measureTheory
> (measure_hvgScript.sml): why the Carathéodory's extension theorem
> (CARATHEODORY), with all related definitions and lemmas, are removed?
>
> [CARATHEODORY]
> |- ∀m0.
> algebra (m_space m0,measurable_sets m0) ∧ positive
Hi,
I have a question about the new version of measureTheory
(measure_hvgScript.sml): why the Carathéodory's extension theorem
(CARATHEODORY), with all related definitions and lemmas, are removed?
[CARATHEODORY]
|- ∀m0.
algebra (m_space m0,measurable_sets m0) ∧ positive m0 ∧
