OrderTopology without LinearOrder

Stream: mathlib4

[Yury G. Kudryashov]

Am I right that we do not care about docs4#OrderTopology on a partial order? E.g., it gives a wrong topology on α × β. Is there a better definition that works at least for (indexed) products of linear orders?

[Yaël Dillies]

We talked about this already, right? I think in #maths