of_isFiniteMeasureOnCompacts — Mathlib

English

If α is a topological space that is sigma-compact and μ is a measure finite on compact sets, then μ is sigma-finite.

Русский

Пусть α — топологическое пространство, сигма-ковертируемое (σ-слово), и μ — мера, конечная на компактах; тогда μ сигма-конечна.

LaTeX

$$$[TopologicalSpace\ α] \land [SigmaCompactSpace\ α] \land [IsFiniteMeasureOnCompacts\ μ] \Rightarrow \ sigma\text{-finite}(μ)$$$

Lean4

instance (priority := 100) of_isFiniteMeasureOnCompacts [TopologicalSpace α] [SigmaCompactSpace α] (μ : Measure α)
    [IsFiniteMeasureOnCompacts μ] : SigmaFinite μ :=
  ⟨⟨{   set := compactCovering α
        set_mem := fun _ => trivial
        finite := fun n => (isCompact_compactCovering α n).measure_lt_top
        spanning := iUnion_compactCovering α }⟩⟩
    -- see Note [lower instance priority]

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