mathlib3

e2d165c8 - chore(topology/order/basic): Move (#17860)

chore(topology/order/basic): Move (#17860) Rename `topology.algebra.order.basic` to `topology.order.basic` because it's almost entirely not about algebra.