Theorems · Theorem · measure theory

IsOpen.isEverywherePos

∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α}
  [μ.IsOpenPosMeasure], IsOpen s → μ.IsEverywherePos s

An open set is everywhere positive for a measure which is positive on open sets.

Defined in

Mathlib.MeasureTheory.Measure.EverywherePos

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceMeasureTheory.Measure.IsOpenPosMeasure