Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-23 04:17 a15ae9c5

View on Github →

chore(measure_theory/measurable_space): add simps config for measurable_equiv (#9315) Also add @[ext] lemma and some standard equiv lemmas.

Estimated changes

Modified src/measure_theory/constructions/pi.lean

Modified src/measure_theory/constructions/prod.lean

Modified src/measure_theory/measurable_space.lean

added theorem measurable_equiv.apply_symm_apply

deleted theorem measurable_equiv.coe_eq

deleted theorem measurable_equiv.coe_symm_mk

added theorem measurable_equiv.coe_to_equiv

added theorem measurable_equiv.coe_to_equiv_symm

added theorem measurable_equiv.ext

added theorem measurable_equiv.self_trans_symm

added def measurable_equiv.simps.apply

added def measurable_equiv.simps.symm_apply

modified def measurable_equiv.symm

added theorem measurable_equiv.symm_apply_apply

added theorem measurable_equiv.symm_mk

added theorem measurable_equiv.symm_refl

added theorem measurable_equiv.symm_trans_self

added theorem measurable_equiv.to_equiv_injective

modified def measurable_equiv.trans

Modified src/measure_theory/measure/measure_space.lean