Theorems · Theorem · measure theory

isCompact_setOfPred_finiteMeasure_le_of_compactSpace

∀ (E : Type u_1) [inst : MeasurableSpace E] [inst_1 : TopologicalSpace E] [T2Space E] [inst_3 : BorelSpace E]
  [CompactSpace E] (C : NNReal), IsCompact {μ | μ.mass ≤ C}

In a compact space, the set of finite measures with mass at most C is compact.

Defined in

Mathlib.MeasureTheory.Measure.Prokhorov

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceT2SpaceBorelSpaceCompactSpace