Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-05 10:56 bda091dd

View on Github →

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.

Estimated changes

Created src/measure_theory/card_measurable_space.lean

added theorem measurable_space.cardinal_Union_generate_measurable_rec_le

added theorem measurable_space.cardinal_generate_measurable_le

added theorem measurable_space.cardinal_generate_measurable_le_continuum

added theorem measurable_space.cardinal_generate_measurable_rec_le

added theorem measurable_space.cardinal_measurable_set_le

added theorem measurable_space.cardinal_measurable_set_le_continuum

added def measurable_space.generate_measurable_rec

added theorem measurable_space.generate_measurable_subset_rec

Modified src/set_theory/cardinal.lean

modified theorem cardinal.power_le_power_left

added theorem cardinal.self_le_power

Modified src/set_theory/cardinal_ordinal.lean

added theorem cardinal.add_le_of_le

added theorem cardinal.omega_lt_aleph_one

Modified src/set_theory/cofinality.lean

added theorem cardinal.is_regular_aleph_one

Modified src/set_theory/continuum.lean

added theorem cardinal.aleph_one_le_continuum

Modified src/set_theory/ordinal.lean