Theorems · Theorem · measure theory

MeasureTheory.Measure.mem_support_restrict

∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [OpensMeasurableSpace X] {s : Set X} {x : X},
  x ∈ (μ.restrict s).support ↔ ∃ᶠ (u : Set X) in (nhdsWithin x s).smallSets, 0 < μ u

Defined in

Mathlib.MeasureTheory.Measure.Support

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceOpensMeasurableSpace