Locally null images #
This file provides a local-to-global criterion for the image of a set to have measure zero.
Main results #
TauCeti.measure_image_null_of_locally_null: an image is null as soon as it is locally null.
theorem
TauCeti.measure_image_null_of_locally_null
{E : Type u_1}
{F : Type u_2}
{G : Type u_3}
[TopologicalSpace E]
[SecondCountableTopology E]
[FunLike G (Set F) ENNReal]
[MeasureTheory.OuterMeasureClass G F]
{ν : G}
{f : E → F}
{s : Set E}
(h : ∀ x ∈ s, ∃ u ∈ nhdsWithin x s, ν (f '' u) = 0)
:
If every point of s has a neighbourhood within s whose image under f is null, then the
image of s is null. A countable subcover, available because the source is second countable,
reduces the global statement to the local ones; this is the image version of
MeasureTheory.measure_null_of_locally_null.