Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-02 17:58 c46a04a3

View on Github →

chore(measure_theory): move, deduplicate (#9489)

move lemmas like is_compact.measure_lt_top from measure_theory.constructions.borel to measure_theory.measure.measure_space;
drop is_compact.is_finite_measure etc;
add measure_Ixx_lt_top.

Estimated changes

Modified src/measure_theory/constructions/borel_space.lean

deleted theorem is_compact.exists_open_superset_measure_lt_top'

deleted theorem is_compact.exists_open_superset_measure_lt_top

deleted theorem is_compact.measure_lt_top

deleted theorem is_compact.measure_lt_top_of_nhds_within

deleted def measure_theory.measure.finite_spanning_sets_in_compact

deleted def measure_theory.measure.finite_spanning_sets_in_open

Modified src/measure_theory/measure/measure_space.lean

added theorem is_compact.exists_open_superset_measure_lt_top'

added theorem is_compact.exists_open_superset_measure_lt_top

deleted theorem is_compact.is_finite_measure

deleted theorem is_compact.is_finite_measure_of_nhds_within

added theorem is_compact.measure_lt_top

added theorem is_compact.measure_lt_top_of_nhds_within

added theorem measure_Icc_lt_top

added theorem measure_Ico_lt_top

added theorem measure_Ioc_lt_top

added theorem measure_Ioo_lt_top

added def measure_theory.measure.finite_spanning_sets_in_compact

added def measure_theory.measure.finite_spanning_sets_in_open

deleted theorem metric.bounded.is_finite_measure

added theorem metric.bounded.measure_lt_top