sigmaFinite_restrict_sigmaFiniteSetGE

English

Let μ and ν be measures on α with ν finite. Then for every natural number n, the restriction of μ to the set μ.sigmaFiniteSetGE(ν, n) is sigma-finite.

Русский

Пусть μ и ν — меры на α, при этом ν конечна. Тогда для любого натурального числа n ограничение μ к совокупности μ.sigmaFiniteSetGE(ν, n) является сигма-финитной.

LaTeX

$$$$\SigmaFinite\left(\mu\restriction\left(\mu\sigmaFiniteSetGE(\nu, n)\right)\right)$$$$

Lean4

theorem sigmaFinite_restrict_sigmaFiniteSetGE (μ ν : Measure α) [IsFiniteMeasure ν] (n : ℕ) :
    SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n)) :=
  (exists_isSigmaFiniteSet_measure_ge μ ν n).choose_spec.2.1

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