English
Let μ and ν be measures with ν finite. Then the ν-measure of μ.sigmaFiniteSetGE(ν, n) is bounded above by the supremum over all ν-measured sets s with μ|s sigma-finite.
Русский
Пусть μ и ν — меры с ν конечной. Тогда мера ν множества μ.sigmaFiniteSetGE(ν, n) не превосходит верхней грань по всем измеримым множествам s, для которых μ|s сигма-финитна.
LaTeX
$$$$\nu\left(\mu\sigmaFiniteSetGE(\nu, n)\right) \le \bigvee_{s:\text{MeasurableSet},\ \SigmaFinite(\mu\restriction s)} \nu(s).$$$$
Lean4
theorem measure_sigmaFiniteSetGE_le (μ ν : Measure α) [IsFiniteMeasure ν] (n : ℕ) :
ν (μ.sigmaFiniteSetGE ν n) ≤ ⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s :=
by
refine (le_iSup (f := fun s ↦ _) (sigmaFinite_restrict_sigmaFiniteSetGE μ ν n)).trans ?_
exact
le_iSup₂ (f := fun s _ ↦ ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) (μ.sigmaFiniteSetGE ν n)
(measurableSet_sigmaFiniteSetGE n)
