Commit 2022-07-15 10:49 72d7b4eb
View on Github →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) μ.
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) μ.