of_separableSpace_orderTopology — Mathlib

English

If α is a densely ordered linear order with order topology and is separable, then α has a countable base.

Русский

Если α—плотно упорядоченная линейная порядковая топология и разделима, то у α счётная база.

LaTeX

$$SecondCountableTopology α$$

Lean4

/-- Let `α` be a densely ordered linear order with order topology. If `α` is a separable space, then
it has second countable topology. Note that the "densely ordered" assumption cannot be dropped, see
[double arrow space](https://topology.pi-base.org/spaces/S000093) for a counterexample. -/
theorem of_separableSpace_orderTopology [OrderTopology α] [DenselyOrdered α] [SeparableSpace α] :
    SecondCountableTopology α := by
  rcases exists_countable_dense α with ⟨s, hc, hd⟩
  refine ⟨⟨_, ?_, hd.topology_eq_generateFrom⟩⟩
  exact (hc.image _).union (hc.image _)

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