Example of a linear order which is a separable space but is not a second countable topology

In this file we provide an example of a linear order such that the order topology is a separable space but is not a second countable topology.

The example is ℝ ×ₗ Bool which is the real line with each point duplicated so that the duplicate is greater than the original point and points with different real values are compared by these values.

instance RealProdLexBool.instTopologicalSpace : TopologicalSpace (Lex (ℝ × Bool))

Equations

• RealProdLexBool.instTopologicalSpace = Preorder.topology (Lex (ℝ × Bool))

instance RealProdLexBool.instOrderTopology : OrderTopology (Lex (ℝ × Bool))

noncomputable instance RealProdLexBool.instLinearOrder : LinearOrder (Lex (ℝ × Bool))

Equations

• RealProdLexBool.instLinearOrder = inferInstance

instance RealProdLexBool.instSeparableSpace : TopologicalSpace.SeparableSpace (Lex (ℝ × Bool))

theorem RealProdLexBool.not_secondCountableTopology : ¬SecondCountableTopology (Lex (ℝ × Bool))