countablySeparated_of_separatesPoints

English

If α is CountablyGenerated and SeparatesPoints, then α is CountablySeparated.

Русский

Если α является CountablyGenerated и SeparationPoints, тогда α является CountablySeparated.

LaTeX

$$$ (\\text{CountablyGenerated } \\alpha) \\land (SeparatesPoints \\alpha) \\Rightarrow CountablySeparated \\alpha $$$

Lean4

instance countablySeparated_of_separatesPoints [MeasurableSpace α] [h : CountablyGenerated α] [SeparatesPoints α] :
    CountablySeparated α := by
  rcases h with ⟨b, hbc, hb⟩
  refine ⟨⟨b, hbc, fun t ht ↦ hb.symm ▸ .basic t ht, ?_⟩⟩
  rw [hb] at ‹SeparatesPoints _›
  convert separating_of_generateFrom b
  simp

Похожие утверждения