[Merged by Bors] - refactor(topology/algebra/ordered): reduce imports

[semorrison]

Renames topology.algebra.ordered to topology.algebra.order, and moves the material about liminf/limsup and about extend_from to separate files, in order to delay imports.

---

[fpvandoorn]

I'm used to default.lean usually importing all files in that directory, and basic.lean containing the basic definitions. So I would expect topology/algebra/order/default.lean to be called topology/algebra/order/basic.lean.
But I believe this is not a (hard) rule in mathlib, so I can also live with this choice.

[PatrickMassot]

I think the new file name is pretty confusing because we already have topology/order which is about the order on tolopological_space X for any X whereas topology/algebra/ordered is about topological_space X assuming X is ordered. I'm not saying the names are great, but having different names seems reasonable.

[semorrison]

I've switched back to ordered per @PatrickMassot's suggestion, and renamed default.lean to basic.lean.

(I might argue that we should get rid of all our "default imports everything" files, but not here.)

[PatrickMassot]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests