isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure

English

If μ is locally finite, then μ is finite on all compact sets; and if the space is compact, then μ finite on compacts implies μ is finite.

Русский

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

LaTeX

$$$$\text{If } \text{IsLocallyFiniteMeasure}(\mu)\text{ then } μ\text{ is finite on compact sets. Conversely, if } α\text{ is compact, then finite on compacts }\iff μ\text{ finite}.$$$$

Lean4

instance (priority := 100) isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure [TopologicalSpace α]
    {_ : MeasurableSpace α} {μ : Measure α} [IsLocallyFiniteMeasure μ] : IsFiniteMeasureOnCompacts μ :=
  ⟨fun _s hs => hs.measure_lt_top_of_nhdsWithin fun _ _ => μ.finiteAt_nhdsWithin _ _⟩

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