Theorems · Theorem · measure theory

MeasureTheory.exists_ne_forall_mem_nhds_pos_measure_preimage

∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [inst : TopologicalSpace β]
  [T1Space β] [SecondCountableTopology β] [Nonempty β] {f : α → β},
  (∀ (b : β), ∃ᵐ (x : α) ∂μ, f x ≠ b) → ∃ a b, a ≠ b ∧ (∀ s ∈ nhds a, 0 < μ (f ⁻¹' s)) ∧ ∀ t ∈ nhds b, 0 < μ (f ⁻¹' t)

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.Measure.Typeclasses.Finite

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceT1SpaceSecondCountableTopologyNonempty