mathlib

mathlib copied to clipboard

The long line is often used as a counterexample in topology.

It can be defined as lex ℝ (Ico (0 : ℝ) 1) which is already equipped with its order thanks to order.lexicographic and a topology thanks to preorder.topology.

Relatingly, one could also study the long ray, the one-point compactification of the long line, the extended long line... Those should all essentially be the same.