English
If α is a measurable space with CountablySeparated, there exists a coarser countably generated measurable space m' such that m' ≤ m and m' separates points.
Русский
Если у измеримого пространства α есть счетчивое разделение, существует более грубое счетчиво порожденное измеримое пространство m', удовлетворяющее m' ≤ m и которое разделяет точки.
LaTeX
$$$ \\exists m' : MeasurableSpace α, CountablyGenerated α \\land SeparatesPoints α \\land m' ≤ m $$$
Lean4
/-- If a measurable space admits a countable separating family of measurable sets,
there is a countably generated coarser space which still separates points. -/
theorem exists_countablyGenerated_le_of_countablySeparated [m : MeasurableSpace α] [h : CountablySeparated α] :
∃ m' : MeasurableSpace α, @CountablyGenerated _ m' ∧ @SeparatesPoints _ m' ∧ m' ≤ m :=
by
rcases h with ⟨b, bct, hbm, hb⟩
refine ⟨generateFrom b, ?_, ?_, generateFrom_le hbm⟩
· use b
rw [@separatesPoints_iff]
exact fun x y hxy ↦ hb _ trivial _ trivial fun _ hs ↦ hxy _ <| measurableSet_generateFrom hs
