instSigmaFinite — Mathlib

English

If α is countable and has a measurable singleton structure, then the counting measure on α is sigma-finite.

Русский

Если множество α счётно и существует измеримая единичка, то счётная мера на α резко является сигма-конечностью.

LaTeX

$$$\Sigma\text{-finite}(\text{count}:\text{Measure }\alpha)$$$

Lean4

instance instSigmaFinite [MeasurableSingletonClass α] [Countable α] : SigmaFinite (count : Measure α) := by
  simp [sigmaFinite_iff_measure_singleton_lt_top]

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