Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-14 10:02 2245cfb6

View on Github →

feat(measurable_space): infix notation for measurable_equiv (#5329) We use ≃ᵐ as notation. Note: ≃ₘ is already used for diffeomorphisms.

Estimated changes

Modified src/measure_theory/borel_space.lean

modified def ennreal.ennreal_equiv_sum

modified def homemorph.to_measurable_equiv

modified def measurable_equiv.ennreal_equiv_nnreal

Modified src/measure_theory/measurable_space.lean

modified theorem measurable_equiv.coe_eq

modified def measurable_equiv.prod_assoc

modified def measurable_equiv.prod_comm

modified def measurable_equiv.prod_congr

modified def measurable_equiv.refl

modified def measurable_equiv.set.prod

modified def measurable_equiv.set.range_inl

modified def measurable_equiv.set.range_inr

modified def measurable_equiv.set.singleton

modified def measurable_equiv.set.univ

modified def measurable_equiv.sum_congr

modified def measurable_equiv.symm

modified def measurable_equiv.trans