Commit 2023-12-20 13:39 fdfe843b

feat(MeasureTheory): define semi-rings of sets (#8867) A semi-ring of sets C (in the sense of measure theory) is a family of sets containing ∅, stable by intersection and such that for all s, t ∈ C, s \ t is equal to a disjoint union of finitely many sets in C. Part of the formalization of the Kolmogorov Extension theorem.