[Merged by Bors] - feat(measure_theory/measure/measure_space): generalize measure.comap

[RemyDegenne]

Generalize comap to functions verifying injective f ∧ ∀ s, measurable_set s → null_measurable_set (f '' s) μ.

---

The change makes the following sorry true, while it was only true for measurable sets before:

import measure_theory.measure.measure_space_def

variables {V : Type*} [measure_space V] {p : V → Prop} {s : set V}

instance subtype.measure_space : measure_space (subtype p) :=
{ volume := measure.comap subtype.val volume,
  ..subtype.measurable_space }

lemma subtype.volume_univ (hs : null_measurable_set s) : volume (univ : set s) = volume s := sorry

According to @YaelDillies , that result will be useful in #2819 .

[urkud]

I'll see if I had a shorter proof in an old abandoned branch. UPD: yes, I had. I'll push it tonight or in the morning.

[urkud]

@RemyDegenne what do you think about this definition?
bors d+

[bors]

✌️ RemyDegenne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[RemyDegenne]

I wanted to follow what was done for map and keep the linear map. I'll use your definition but I'll put the linear map back in.

[RemyDegenne]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests