isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts

English

A measure finite on compact sets in a locally compact space is locally finite.

Русский

Мера, конечная на компактных множествах в локально компактном пространстве, локально конечна.

LaTeX

$$$IsLocallyFiniteMeasure μ$$$

Lean4

/-- A measure which is finite on compact sets in a locally compact space is locally finite. -/
instance (priority := 100) isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts [TopologicalSpace α]
    [WeaklyLocallyCompactSpace α] [IsFiniteMeasureOnCompacts μ] : IsLocallyFiniteMeasure μ :=
  ⟨fun x ↦
    let ⟨K, K_compact, K_mem⟩ := exists_compact_mem_nhds x
    ⟨K, K_mem, K_compact.measure_lt_top⟩⟩

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