mathlib
62f94ad6 - feat(measure_theory/measurable_space): define `measurable_embedding` (#10023)

Commit

4 years ago

feat(measure_theory/measurable_space): define `measurable_embedding` (#10023) This way we can generalize our theorems about `measurable_equiv` and `closed_embedding`s.

Author

urkud

Parents

c50c2c32

mathlib 62f94ad6 - feat(measure_theory/measurable_space): define `measurable_embedding` (#10023)

mathlib
62f94ad6 - feat(measure_theory/measurable_space): define `measurable_embedding` (#10023)