mathlib

bda091dd - feat(measure_theory/card_measurable_space): cardinality of generated sigma-algebras (#12422)

feat(measure_theory/card_measurable_space): cardinality of generated sigma-algebras (#12422) If a sigma-algebra is generated by a set of sets `s` whose cardinality is at most the continuum, then the sigma-algebra satisfies the same cardinality bound. Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>