The long line

[YaelDillies]

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.

[vihdzp]

I don't think your definition is correct? The long line has the property that every increasing sequence has a limit. What you mention doesn't, at least not under the order topology.

Would it not be better to directly define it as the product aleph 1 × Ico 0 1? In this case, the order topology is what you want.

[j-loreaux]

However, it doesn't yet have a topology!

Do we not have the order topology on linearly ordered types (not as an instance, just a def)?

[YaelDillies]

Oh yes probably. Feel free to edit with the name of the declaration.

[vihdzp]

I should also mention, as of a few months ago, we have a file set_theory/ordinal/topology with a few topological results on ordinals. That would be a great place to add theorems on the long line. Only reason I haven't done so myself is that I'm not much of an expert on the subject matter :(