Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-06 22:22 17a7f69e

View on Github →

doc(measure_theory/ae_eq_fun): add documentations and some lemmas (#1650)

Add documentations. to_fun.
More precise comments

Estimated changes

Modified src/measure_theory/ae_eq_fun.lean

added theorem measure_theory.ae_eq_fun.add_to_fun

added theorem measure_theory.ae_eq_fun.all_ae_mk_to_fun

added theorem measure_theory.ae_eq_fun.comp_edist_to_fun

added theorem measure_theory.ae_eq_fun.comp_eq_mk_to_fun

added theorem measure_theory.ae_eq_fun.comp_mk

added theorem measure_theory.ae_eq_fun.comp_to_fun

added theorem measure_theory.ae_eq_fun.comp₂_eq_mk_to_fun

added theorem measure_theory.ae_eq_fun.comp₂_to_fun

added theorem measure_theory.ae_eq_fun.const_to_fun

added theorem measure_theory.ae_eq_fun.edist_to_fun'

added theorem measure_theory.ae_eq_fun.edist_to_fun

added theorem measure_theory.ae_eq_fun.edist_zero_to_fun

added theorem measure_theory.ae_eq_fun.eintegral_to_fun

added theorem measure_theory.ae_eq_fun.ext

added theorem measure_theory.ae_eq_fun.le_iff_to_fun_le

added theorem measure_theory.ae_eq_fun.lift_rel_iff_to_fun

modified theorem measure_theory.ae_eq_fun.mk_add_mk

added theorem measure_theory.ae_eq_fun.mk_sub_mk

added theorem measure_theory.ae_eq_fun.neg_to_fun

added theorem measure_theory.ae_eq_fun.one_to_fun

added theorem measure_theory.ae_eq_fun.self_eq_mk

added theorem measure_theory.ae_eq_fun.smul_to_fun

added theorem measure_theory.ae_eq_fun.sub_to_fun

added theorem measure_theory.ae_eq_fun.zero_to_fun