Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-07 19:35 99fe12af

View on Github →

refactor(measure_theory/ae_eq_fun): move emetric to ae_eq_fun_metric (#6081) Cherry-picked from #6042

Estimated changes

Modified src/measure_theory/ae_eq_fun.lean

deleted theorem measure_theory.ae_eq_fun.coe_fn_edist

deleted theorem measure_theory.ae_eq_fun.edist_add_right

deleted theorem measure_theory.ae_eq_fun.edist_eq_coe'

deleted theorem measure_theory.ae_eq_fun.edist_eq_coe

deleted theorem measure_theory.ae_eq_fun.edist_mk_mk'

deleted theorem measure_theory.ae_eq_fun.edist_mk_mk

deleted theorem measure_theory.ae_eq_fun.edist_smul

deleted theorem measure_theory.ae_eq_fun.edist_zero_eq_coe

Created src/measure_theory/ae_eq_fun_metric.lean

added theorem measure_theory.ae_eq_fun.coe_fn_edist

added theorem measure_theory.ae_eq_fun.edist_add_right

added theorem measure_theory.ae_eq_fun.edist_eq_coe'

added theorem measure_theory.ae_eq_fun.edist_eq_coe

added theorem measure_theory.ae_eq_fun.edist_mk_mk'

added theorem measure_theory.ae_eq_fun.edist_mk_mk

added theorem measure_theory.ae_eq_fun.edist_smul

added theorem measure_theory.ae_eq_fun.edist_zero_eq_coe

Modified src/measure_theory/l1_space.lean