English
If α is a topological space with second countability and every point x ∈ s has a neighborhood within s of measure zero, then μ(s) = 0.
Русский
Если пространства α вторично счетно, и для каждой точки x ∈ s существует окрестность внутри s с нулевой мерой, то μ(s) = 0.
LaTeX
$$$[TopologicalSpace\\ α] \\\\& [SecondCountableTopology\\ α] \\\\Rightarrow \\\\forall s, \\\\Big(\\\\forall x\\\\in s,\\\\ \\\\exists u, x\\\\in u \\\\subseteq s \\\\wedge μ(u)=0\\\\Big) \\\\Rightarrow μ(s)=0$$$
Lean4
/-- If a set has zero measure in a neighborhood of each of its points, then it has zero measure
in a second-countable space. -/
theorem measure_null_of_locally_null [TopologicalSpace α] [SecondCountableTopology α] (s : Set α)
(hs : ∀ x ∈ s, ∃ u ∈ 𝓝[s] x, μ u = 0) : μ s = 0 :=
by
choose! u hxu hu₀ using hs
choose t ht using TopologicalSpace.countable_cover_nhdsWithin hxu
rcases ht with ⟨ts, t_count, ht⟩
apply measure_mono_null ht
exact (measure_biUnion_null_iff t_count).2 fun x hx => hu₀ x (ts hx)
