isTightMeasureSet_singleton — Mathlib

English

In a compact space, every set of measures is tight.

Русский

В компактном пространстве любая пара множеств мер плотна.

LaTeX

$$[CompactSpace X] ⇒ IsTightMeasureSet S$$

Lean4

/-- In a complete second-countable pseudo-metric space, finite measures are tight. -/
theorem isTightMeasureSet_singleton {α : Type*} {mα : MeasurableSpace α} [PseudoEMetricSpace α] [CompleteSpace α]
    [SecondCountableTopology α] [BorelSpace α] {μ : Measure α} [IsFiniteMeasure μ] : IsTightMeasureSet { μ } :=
  isTightMeasureSet_singleton_of_innerRegularWRT (innerRegular_isCompact_isClosed_measurableSet_of_finite _)

Похожие утверждения