Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-23 18:48 72e5b9fc

View on Github →

feat(measure_theory): ext lemmas for measures (#3895) Add class sigma_finite. Also some cleanup. Rename measurable_space.is_measurable -> measurable_space.is_measurable'. This is to avoid name clash with _root_.is_measurable, which should almost always be used instead. define is_pi_system.

Estimated changes

Modified src/data/set/basic.lean

added theorem set.diff_eq_compl_inter

added theorem set.diff_inter_self_eq_diff

added theorem set.diff_self_inter

Modified src/logic/basic.lean

added theorem fact.elim

Modified src/measure_theory/borel_space.lean

modified theorem measurable.ennreal_add

Modified src/measure_theory/content.lean

Modified src/measure_theory/haar_measure.lean

Modified src/measure_theory/lebesgue_measure.lean

Modified src/measure_theory/measurable_space.lean

modified def is_measurable

added def is_pi_system

modified theorem measurable_space.dynkin_system.generate_from_eq

added theorem measurable_space.dynkin_system.generate_has_compl

added theorem measurable_space.dynkin_system.generate_has_def

added theorem measurable_space.dynkin_system.generate_has_subset_generate_measurable

added theorem measurable_space.ext_iff

modified theorem measurable_space.generate_from_le

modified theorem measurable_space.generate_from_le_iff

modified theorem measurable_space.induction_on_inter

Modified src/measure_theory/measure_space.lean

added theorem measure_theory.ext_of_generate_finite

added theorem measure_theory.measure.ext_of_generate_from_of_Union

modified def measure_theory.measure.is_complete

added theorem measure_theory.measure_compl

Modified src/measure_theory/outer_measure.lean