Commit 2024-08-16 13:44 9c20287c

View on Github →

feat(Topology/Order/LowerUpperTopology): Scott and Upper topologies coincide on a complete linear order (#12234) This PR shows that the subbasis used to define the lower (upper) topology together with the universal set form a basis for the lower (upper) topology on a linear order. When the linear order is complete, the subbasis with the universal set is the topology. A consequence of this result is that the Scott and upper topologies coincide on a complete linear order.

Estimated changes