Theorems · Theorem · measure theory

MeasureTheory.measure_null_of_locally_null

∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F}
  [inst_2 : TopologicalSpace α] [SecondCountableTopology α] (s : Set α),
  (∀ x ∈ s, ∃ u ∈ nhdsWithin x s, μ u = 0) → μ s = 0

If a set has zero measure in a neighborhood of each of its points, then it has zero measure in a second-countable space.

Defined in

Mathlib.MeasureTheory.OuterMeasure.Basic

Cited by

5 results in Mathlib

Foundations

Depth 132 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FunLikeMeasureTheory.OuterMeasureClassTopologicalSpaceSecondCountableTopology