isFiniteMeasure_iff_isFiniteMeasureOnCompacts_of_compactSpace

English

On a compact space, μ is finite iff μ is finite on compact sets.

Русский

На компактном пространстве мера μ конечна тогда и только тогда, когда она конечна на компактных множествах.

LaTeX

$$$$IsFiniteMeasure(\mu) \;\Leftrightarrow\; IsFiniteMeasureOnCompacts(\mu)$$$$

Lean4

theorem isFiniteMeasure_iff_isFiniteMeasureOnCompacts_of_compactSpace [TopologicalSpace α] [MeasurableSpace α]
    {μ : Measure α} [CompactSpace α] : IsFiniteMeasure μ ↔ IsFiniteMeasureOnCompacts μ :=
  by
  constructor <;> intros
  · infer_instance
  · exact CompactSpace.isFiniteMeasure

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