instSigmaFiniteRestrictUnionSet — Mathlib

English

If μ i are sigma-finite for all i in a finite index set, then sum μ is sigma-finite.

Русский

Если для всех i в конечном наборе индексов μ i сигма-конечна, то сумма μ по i сигма-конечна.

LaTeX

$$instance sigmaFinite {ι} [Finite ι] (μ : ι → Measure α) [∀ i, SigmaFinite (μ i)] : SigmaFinite (sum μ)$$

Lean4

instance [SigmaFinite (μ.restrict s)] [SigmaFinite (μ.restrict t)] : SigmaFinite (μ.restrict (s ∪ t)) :=
  sigmaFinite_of_le _ (restrict_union_le _ _)

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