mathlib3
09fa0b0c - refactor(measure_theory/measurable_space): utilize measurable_embedding more (#17980)

Commit
3 years ago
refactor(measure_theory/measurable_space): utilize measurable_embedding more (#17980) Change the hypothesis in `measurable_equiv.set.image` and `measurable_equiv.set.range` to use `measurable_embedding`. Also remove measurable_embedding.equiv_range which is redundant.
Parents
Loading