Theorems · Definition · measure theory

MeasureTheory.Measure.support

{X : Type u_1} → [TopologicalSpace X] → [inst : MeasurableSpace X] → MeasureTheory.Measure X → Set X

A point x is in the support of μ if any open neighborhood of x has positive measure. We provide the definition in terms of the filter-theoretic equivalent ∃ᶠ u in (𝓝 x).smallSets, 0 < μ u.

Defined in

Mathlib.MeasureTheory.Measure.Support

Cited by

41 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpace