sigmaFinite — Mathlib

English

A Haar measure on a σ-compact space is σ-finite.

Русский

Мера Хаара на σ-компактном пространстве σ-конечна.

LaTeX

$$$\\exists (A_n)_{n\\in\\mathbb{N}}, \\bigcup_{n} A_n = G \\wedge \\forall n, \\mu(A_n) < \\infty$$$

Lean4

/-- A Haar measure on a σ-compact space is σ-finite.

See Note [lower instance priority] -/
@[to_additive /-- A Haar measure on a σ-compact space is σ-finite.

    See Note [lower instance priority] -/
    ]
instance (priority := 100) sigmaFinite [SigmaCompactSpace G] : SigmaFinite μ :=
  ⟨⟨{   set := compactCovering G
        set_mem := fun _ => mem_univ _
        finite := fun n => IsCompact.measure_lt_top <| isCompact_compactCovering G n
        spanning := iUnion_compactCovering G }⟩⟩

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