English
If X is countably generated and μ is s-finite, then μ is separable.
Русский
Если пространство X счетно генерируемо, а μ — s-ограниченная мера, то μ разделима.
LaTeX
$$$$\\text{CountablyGenerated X} \\;\\wedge\\; \\text{SFinite } μ \\;\\Longrightarrow\\; \\text{IsSeparable } μ.$$$$
Lean4
/-- If a measurable space is countably generated and equipped with an s-finite measure, then the
measure is separable. -/
instance [CountablyGenerated X] [SFinite μ] : IsSeparable μ where
exists_countable_measureDense :=
by
have := isSeparable_of_sigmaFinite (μ.restrict μ.sigmaFiniteSet)
rcases exists_countable_measureDense (μ.restrict μ.sigmaFiniteSet) with ⟨𝒜, count_𝒜, h𝒜⟩
let ℬ := {s ∩ μ.sigmaFiniteSet | s ∈ 𝒜}
refine ⟨ℬ, count_𝒜.image (fun s ↦ s ∩ μ.sigmaFiniteSet), ?_, ?_⟩
· rintro - ⟨s, s_mem, rfl⟩
exact (h𝒜.measurable s s_mem).inter measurableSet_sigmaFiniteSet
· intro s ms hμs ε ε_pos
rcases restrict_compl_sigmaFiniteSet_eq_zero_or_top μ s with hs | hs
· have : (μ.restrict μ.sigmaFiniteSet) s ≠ ∞ := ne_top_of_le_ne_top hμs <| μ.restrict_le_self _
rcases h𝒜.approx s ms this ε ε_pos with ⟨t, t_mem, ht⟩
refine ⟨t ∩ μ.sigmaFiniteSet, ⟨t, t_mem, rfl⟩, ?_⟩
have : μ (s ∆ (t ∩ μ.sigmaFiniteSet) \ μ.sigmaFiniteSet) = 0 :=
by
rw [diff_eq_compl_inter, inter_symmDiff_distrib_left, ← ENNReal.bot_eq_zero, eq_bot_iff]
calc
μ ((μ.sigmaFiniteSetᶜ ∩ s) ∆ (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet))) ≤
μ ((μ.sigmaFiniteSetᶜ ∩ s) ∪ (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet))) :=
measure_mono symmDiff_subset_union
_ ≤ μ (μ.sigmaFiniteSetᶜ ∩ s) + μ (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) := (measure_union_le _ _)
_ = 0 := by
rw [inter_comm, ← μ.restrict_apply ms, hs, ← inter_assoc, inter_comm, ← inter_assoc, inter_compl_self,
empty_inter, measure_empty, zero_add]
rwa [← measure_inter_add_diff _ measurableSet_sigmaFiniteSet, this, add_zero, inter_symmDiff_distrib_right,
inter_assoc, inter_self, ← inter_symmDiff_distrib_right, ← μ.restrict_apply' measurableSet_sigmaFiniteSet]
· refine False.elim <| hμs ?_
rw [eq_top_iff, ← hs]
exact μ.restrict_le_self _
