Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-23 01:49 542d06a6

View on Github →

feat(measure_theory): use pseudo_metrizable_space instead of metrizable_space (#14310)

Estimated changes

Modified src/measure_theory/function/ae_eq_fun.lean

modified theorem measure_theory.ae_eq_fun.comp_measurable_to_germ

Modified src/measure_theory/function/simple_func_dense.lean

Modified src/measure_theory/function/strongly_measurable.lean

modified theorem ae_measurable.ae_strongly_measurable

modified theorem ae_strongly_measurable_Union_iff

modified theorem ae_strongly_measurable_add_measure_iff

modified theorem ae_strongly_measurable_id

modified theorem ae_strongly_measurable_iff_ae_measurable

modified theorem ae_strongly_measurable_union_iff

modified theorem exists_strongly_measurable_limit_of_tendsto_ae

modified theorem measurable.strongly_measurable

modified theorem measure_theory.ae_strongly_measurable.add_measure

modified theorem measure_theory.ae_strongly_measurable.measurable_mk

modified theorem measure_theory.ae_strongly_measurable.sum_measure

modified theorem strongly_measurable_id

Modified src/measure_theory/group/fundamental_domain.lean

Modified src/measure_theory/integral/bochner.lean

Modified src/measure_theory/integral/integrable_on.lean

Modified src/measure_theory/integral/integral_eq_improper.lean

modified theorem measure_theory.ae_cover.ae_strongly_measurable