mathlib3
2245cfb6 - feat(measurable_space): infix notation for measurable_equiv (#5329)

Commit

5 years ago

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

Author

fpvandoorn

Parents