Commit 2025-01-24 07:58 8a9bd060

feat(MeasureTheory): additive contents on rings of sets (#20977) Two main results:

• a function on a ring of sets which is additive on pairs of disjoint sets defines an additive content
• if an additive content is continuous at ∅, then its value on a countable disjoint union is the sum of the values Part of the formalization of Kolmogorov's extension theorem.