Theorems · Theorem · measure theory

IsMeagre.of_isSigmaCompact_null

∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {s : Set X} {μ : MeasureTheory.Measure X}
  [μ.IsOpenPosMeasure] [T2Space X], IsSigmaCompact s → μ s = 0 → IsMeagre s

A σ-compact measure zero subset is meagre. (More generally, every Fσ set of measure zero is meagre.)

Defined in

Mathlib.MeasureTheory.Measure.OpenPos

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceMeasureTheory.Measure.IsOpenPosMeasureT2Space