mathlib

72d7b4eb - feat(measure_theory/measure/measure_space): generalize measure.comap (#15343)

feat(measure_theory/measure/measure_space): generalize measure.comap (#15343) Generalize comap to functions verifying `injective f ∧ ∀ s, measurable_set s → null_measurable_set (f '' s) μ`. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>