measure_sigmaFiniteSetGE_ge — Mathlib

English

Under ν finite, the supremum of ν(s) over all measurable s with μ|s sigma-finite, minus 1/n is a lower bound for ν(μ.sigmaFiniteSetGE(ν, n)).

Русский

Пусть ν конечна. Тогда верхняя грань ν(s) по всем измеримым s, для которых μ|s сигма-финитна, минус 1/n является нижней границей для ν(μ.sigmaFiniteSetGE(ν, n)).

LaTeX

$$$$\left(\sup_{s:\text{MeasurableSet},\ \SigmaFinite(\mu\restriction s)} \nu(s)\right) - \frac{1}{n} \le \nu\left(\mu\sigmaFiniteSetGE(\nu, n)\right).$$$$

Lean4

theorem measure_sigmaFiniteSetGE_ge (μ ν : Measure α) [IsFiniteMeasure ν] (n : ℕ) :
    (⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / n ≤ ν (μ.sigmaFiniteSetGE ν n) :=
  (exists_isSigmaFiniteSet_measure_ge μ ν n).choose_spec.2.2

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