Theorems · Theorem · measure theory

MeasureTheory.exists_accPt_of_nullSingletonClass

∀ {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [MeasureTheory.NullSingletonClass μ] {E : Set X} [TopologicalSpace.SeparableSpace ↑E],
  0 < μ E → ∃ x, AccPt x (Filter.principal E)

Defined in

Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceMeasureTheory.NullSingletonClassTopologicalSpace.SeparableSpace