sigmaFinite_of_locallyFinite — Mathlib

English

If μ is locally finite and α is second-countable, then μ is sigma-finite.

Русский

Если μ локально конечна и пространство α второй счетности, то μ сигма-конечна.

LaTeX

$$$\text{IsLocallyFiniteMeasure}(μ) \Rightarrow \sigma\text{-finite}(μ)\quad \text{under suitable topological hypotheses}$$$

Lean4

instance (priority := 100) sigmaFinite_of_locallyFinite [TopologicalSpace α] [SecondCountableTopology α]
    [IsLocallyFiniteMeasure μ] : SigmaFinite μ :=
  by
  choose s hsx hsμ using μ.finiteAt_nhds
  rcases TopologicalSpace.countable_cover_nhds hsx with ⟨t, htc, htU⟩
  refine Measure.sigmaFinite_of_countable (htc.image s) (forall_mem_image.2 fun x _ => hsμ x) ?_
  rwa [sUnion_image]

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