sigmaFinite — Mathlib

English

If μ is sigma-finite, then c • μ is sigma-finite for any c ≥ 0 (real nonnegative).

Русский

Если μ сигма-конечна, то для любого c ≥ 0 (в NNReal) c • μ сигма-конечна.

LaTeX

$$instance sigmaFinite {μ : Measure α} [SigmaFinite μ] (c : ℝ≥0) : SigmaFinite (c • μ)$$

Lean4

instance sigmaFinite {μ : Measure α} [SigmaFinite μ] (c : ℝ≥0) : MeasureTheory.SigmaFinite (c • μ) where
  out' :=
    ⟨{  set := spanningSets μ
        set_mem := fun _ ↦ trivial
        finite := by
          intro i
          simp only [Measure.coe_smul, Pi.smul_apply, nnreal_smul_coe_apply]
          exact ENNReal.mul_lt_top ENNReal.coe_lt_top (measure_spanningSets_lt_top μ i)
        spanning := iUnion_spanningSets μ }⟩

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