mathlib3
73423cf9 - feat(measure/measurable_space): add `measurable_equiv.of_unique_of_unique` (#9968)

Commit

4 years ago

feat(measure/measurable_space): add `measurable_equiv.of_unique_of_unique` (#9968) Also fix a typo in a lemma name: `measurable_equiv.measurable_coe_iff` → `measurable_comp_iff`.

Author

urkud

Parents

7f2b8064

mathlib3 73423cf9 - feat(measure/measurable_space): add `measurable_equiv.of_unique_of_unique` (#9968)

mathlib3
73423cf9 - feat(measure/measurable_space): add `measurable_equiv.of_unique_of_unique` (#9968)