English
Any measurable space on a countable set is countably generated.
Русский
Будущее измеримое пространство на счётном множестве считай счётно порождаемо.
LaTeX
$$$ \forall \alpha, [\text{MeasurableSpace } \alpha] \Rightarrow \text{CountablyGenerated } \alpha $$$
Lean4
/-- Any measurable space structure on a countable space is countably generated. -/
instance (priority := 100) [MeasurableSpace α] [Countable α] : CountablyGenerated α where
isCountablyGenerated :=
by
refine ⟨⋃ y, {measurableAtom y}, countable_iUnion (fun i ↦ countable_singleton _), ?_⟩
refine le_antisymm ?_ (generateFrom_le (by simp [MeasurableSet.measurableAtom_of_countable]))
intro s hs
have : s = ⋃ y ∈ s, measurableAtom y := by
apply Subset.antisymm
· intro x hx
simpa using ⟨x, hx, by simp⟩
· simp only [iUnion_subset_iff]
intro x hx
exact measurableAtom_subset hs hx
rw [this]
apply MeasurableSet.biUnion (to_countable s) (fun x _hx ↦ ?_)
apply measurableSet_generateFrom
simp
