Typeclass for ordered topological space unbounded above

Stream: Is there code for X?

[Michael Rothgang]

I'm looking for a typeclass on ordered topological spaces X with the following property:

• for every a : Xthere is an element b : X such that a < b

The real numbers satisfy this, but that seems like a big special case. Does mathlib have a typeclass for this?

[Eric Rodriguez]

docs#NoMaxOrder

[Eric Rodriguez]

there's no need for the space to be topological, although I'm sure there's lemmas with both assumptions

[Michael Rothgang]

Thanks! In my context, I want to talk about continuous functions into such a domain - so I'll need a topology anyway.

[Yury G. Kudryashov]

Then you add [TopologicalSpace X] and possibly [OrderTopology X] to the assumptions.

[Michael Rothgang]

My context is #9872 (just one lemma, 7 lines lines :-)), which already has these in the context.