English
Let m ≤ m0 and m₂ ≤ m, and the trimmed measure μ.trim (m₂.trans m) is sigma-finite. Then μ.trim m is sigma-finite.
Русский
Пусть m ≤ m0 и m₂ ≤ m, и урезанная мера μ.trim (m₂.trans m) сигма-конечна. Тогда μ.trim m сигма-конечна.
LaTeX
$$$\\Sigma$-finite( $\\mu$ trim $hm$ ) если $hm: m \\le m_0$, $hm_2: m_2 \\le m$, и $\\Sigma$-finite$(\\mu trim (hm_2.trans hm))$.$$
Lean4
theorem sigmaFiniteTrim_mono {m m₂ m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) (hm₂ : m₂ ≤ m)
[SigmaFinite (μ.trim (hm₂.trans hm))] : SigmaFinite (μ.trim hm) :=
by
refine ⟨⟨?_⟩⟩
refine
{ set := spanningSets (μ.trim (hm₂.trans hm))
set_mem := fun _ => Set.mem_univ _
finite := fun i => ?_
spanning := iUnion_spanningSets _ }
calc
(μ.trim hm) (spanningSets (μ.trim (hm₂.trans hm)) i) =
((μ.trim hm).trim hm₂) (spanningSets (μ.trim (hm₂.trans hm)) i) :=
by rw [@trim_measurableSet_eq α m₂ m (μ.trim hm) _ hm₂ (measurableSet_spanningSets _ _)]
_ = (μ.trim (hm₂.trans hm)) (spanningSets (μ.trim (hm₂.trans hm)) i) := by rw [@trim_trim _ _ μ _ _ hm₂ hm]
_ < ∞ := measure_spanningSets_lt_top _ _
