English
If X is countably generated and μ is σ-finite, then μ is a separable measure.
Русский
Если пространство X счетно-генерируемо и μ является σ-конечным, то μ является separable.
LaTeX
$$$$\\text{CountablyGenerated } X \\;\\wedge\\; \\text{SigmaFinite } μ \\;\Longrightarrow\\; \\text{IsSeparable } μ.$$$$
Lean4
/-- If a measurable space is countably generated and equipped with a `σ`-finite measure, then the
measure is separable. This is not an instance because it is used below to prove the more
general case where `μ` is s-finite. -/
theorem isSeparable_of_sigmaFinite [CountablyGenerated X] [SigmaFinite μ] : IsSeparable μ where
exists_countable_measureDense := by
have h := countable_countableGeneratingSet (α := X)
have hgen := generateFrom_countableGeneratingSet (α := X)
let 𝒜 := (countableGeneratingSet X) ∪ {μ.toFiniteSpanningSetsIn.set n | n : ℕ}
have count_𝒜 : 𝒜.Countable :=
countable_union.2 ⟨h, countable_iff_exists_subset_range.2 ⟨μ.toFiniteSpanningSetsIn.set, fun _ hx ↦ hx⟩⟩
refine
⟨generateSetAlgebra 𝒜, countable_generateSetAlgebra count_𝒜,
Measure.MeasureDense.of_generateFrom_isSetAlgebra_sigmaFinite isSetAlgebra_generateSetAlgebra
{ set := μ.toFiniteSpanningSetsIn.set
set_mem := fun n ↦ self_subset_generateSetAlgebra (𝒜 := 𝒜) <| Or.inr ⟨n, rfl⟩
finite := μ.toFiniteSpanningSetsIn.finite
spanning := μ.toFiniteSpanningSetsIn.spanning } (le_antisymm ?_ (generateFrom_le (fun s hs ↦ ?_)))⟩
· rw [← hgen]
exact
generateFrom_mono <| le_trans self_subset_generateSetAlgebra <| generateSetAlgebra_mono <| subset_union_left ..
·
induction hs with
| base t t_mem =>
rcases t_mem with t_mem | ⟨n, rfl⟩
· exact hgen ▸ measurableSet_generateFrom t_mem
· exact μ.toFiniteSpanningSetsIn.set_mem n
| empty => exact MeasurableSet.empty
| compl t _ t_mem => exact MeasurableSet.compl t_mem
| union t u _ _ t_mem u_mem => exact MeasurableSet.union t_mem u_mem
