Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-03 14:09 b2be1eeb

View on Github →

feat(measure_theory/measure_space): add 3 typeclasses (#3664) Define probability_measure, finite_measure, and locally_finite_measure.

Estimated changes

Modified src/analysis/special_functions/pow.lean

Modified src/data/real/ennreal.lean

added theorem ennreal.one_lt_top

Modified src/measure_theory/integration.lean

modified theorem measure_theory.simple_func.lintegral_congr

Modified src/measure_theory/measure_space.lean

added theorem is_compact.finite_measure

added theorem measure_theory.ae_mono

added theorem measure_theory.ae_restrict_iff

added theorem measure_theory.finite_at_filter_of_finite

added theorem measure_theory.measure.finite_at_filter.filter_mono

added theorem measure_theory.measure.finite_at_filter.filter_mono_ae

added theorem measure_theory.measure.finite_at_filter.filter_sup

added theorem measure_theory.measure.finite_at_filter.inf_ae_iff

added theorem measure_theory.measure.finite_at_filter.inf_of_left

added theorem measure_theory.measure.finite_at_filter.inf_of_right

added def measure_theory.measure.finite_at_filter

added theorem measure_theory.measure.finite_at_nhds

added theorem measure_theory.measure.finite_at_nhds_within

added theorem measure_theory.measure.finite_at_principal

added theorem measure_theory.measure.le_sum

modified theorem measure_theory.measure_congr

deleted theorem measure_theory.measure_diff_of_ae_imp

added theorem measure_theory.measure_diff_of_ae_le

deleted theorem measure_theory.measure_le_of_ae_imp

added theorem measure_theory.measure_mono_ae

added theorem measure_theory.restrict_congr

added theorem measure_theory.restrict_mono_ae

added theorem metric.bounded.finite_measure

Modified src/order/filter/basic.lean

added theorem filter.eventually_eq.filter_mono

deleted theorem filter.eventually_eq.mem_iff

added theorem filter.eventually_eq_set

deleted theorem filter.eventually_set_ext