Theorems · Theorem · general topology

SecondCountableTopology.of_separableSpace_orderTopology

∀ (α : Type u) [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [TopologicalSpace.SeparableSpace α], SecondCountableTopology α

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.

Defined in

Mathlib.Topology.Order.Basic

Cited by

0 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceLinearOrderOrderTopologyDenselyOrderedTopologicalSpace.SeparableSpace