English
In a σ-finite μ, if s is measurable with μ s > r, there exists a measurable t ⊆ s with r < μ t < ∞.
Русский
В σ‑конечной μ, если s измеримо и μ(s) > r, то существует измеримое t ⊆ s такое, что r < μ(t) < ∞.
LaTeX
$$$[SigmaFinite μ] \; {r : \mathbb{R}_{\ge 0}^{\infty}} (hs : MeasurableSet s) (h's : r < μ s) : \exists t, MeasurableSet t ∧ t \subseteq s ∧ r < μ t ∧ μ t < \infty$$$
Lean4
/-- In a σ-finite space, any measurable set of measure `> r` contains a measurable subset of
finite measure `> r`. -/
theorem exists_subset_measure_lt_top [SigmaFinite μ] {r : ℝ≥0∞} (hs : MeasurableSet s) (h's : r < μ s) :
∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < μ t ∧ μ t < ∞ :=
by
rw [← iSup_restrict_spanningSets, @lt_iSup_iff _ _ _ r fun i : ℕ => μ.restrict (spanningSets μ i) s] at h's
rcases h's with ⟨n, hn⟩
simp only [restrict_apply hs] at hn
refine ⟨s ∩ spanningSets μ n, hs.inter (measurableSet_spanningSets _ _), inter_subset_left, hn, ?_⟩
exact (measure_mono inter_subset_right).trans_lt (measure_spanningSets_lt_top _ _)
