of_compactSpace — Mathlib

English

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

Русский

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

LaTeX

$$$\text{CompactSpace}(X) \Rightarrow \IsTightMeasureSet(S)$$$

Lean4

/-- In a compact space, every set of measures is tight. -/
theorem of_compactSpace [CompactSpace 𝓧] : IsTightMeasureSet S :=
  by
  simp only [IsTightMeasureSet, cocompact_eq_bot, smallSets_bot, tendsto_pure_left, iSup_apply, measure_empty,
    ENNReal.iSup_zero, ciSup_const]
  exact fun _ ↦ mem_of_mem_nhds

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