Commit 2023-12-07 22:44 049f6f9c

feat: Scott topology on a preorder (#2508) Introduce the Scott topology on a preorder, defined in terms of directed sets. There is already a related notion of Scott topology defined in topology.omega_complete_partial_order, where it is defined on ω-complete partial orders in terms of ω-chains. In some circumstances the definition given here coincides with that given in topology.omega_complete_partial_order but in general they are different. Abramsky and Jung ([Domain Theory, 2.2.4][abramsky_gabbay_maibaum_1994]) argue that the ω-chain approach has pedagogical advantages, but the directed sets approach is more appropriate as a theoretical foundation.