null_of_locally_null

Stream: maths

[Yury G. Kudryashov]

@Sebastien Gouezel I see that the assumption of docs#measure_theory.null_of_locally_null intersects with s twice: first when it says that u belongs to neighborhoods within s, then once more explicitly.

[Yury G. Kudryashov]

Is it intentional?

[Sebastien Gouezel]

No, I don't think it's intentional. The lemma is perfectly usable as it is now, though, and removing one intersection or the other would arguably make it weaker formally, so I don't know if it's worth changing. Don't hesitate to PR a change if you think another version is easier to use!

[Yury G. Kudryashov]

I'm going to move it to outer_measure anyway (so that applying it to map f μ doesn't require f to be measurable). I'll make a PR later today or tomorrow.

[Yury G. Kudryashov]

I use it to prove that a function is either a.e.-constant, or admits two disjoint balls in the codomain such that the preimages of both balls have positive measure (and I'm going to use this that in case of a strictly convex codomain, ∥∫ x, f x∥ < ∫ x, ∥f x∥ unless f is a.e.-constant).