Commit 2024-05-04 19:06 8122c5d8

feat(Topology/Order/LawsonTopology): Introduce the Lawson Topology to Mathlib (#11710) Introduces the Lawson Topology on a preorder. The Lawson Topology is defined as the meet of the Lower Topology and the Scott Topology previously introduced. A basis for the Lawson Topology is defined and some basic results are established:

• An upper set is Lawson open if and only if it is Scott open
• A lower set is Lawson closed if and only if it is closed under sups of directed sets
• The Lawson topology on a partial order is T₀