Commit 2023-01-21 10:44 38fe3f3c

feat(topology/order/lower_topology): Introduce the lower topology on a preorder (#17426) This PR introduces the lower topology on a preorder. It is shown that the lower topology on a partial order is T₀ and the non-empty complements of the upper closures of finite subsets form a basis. It is also shown that the lower topology on the product of two order_bot spaces coincides with the product topology of the lower topologies on the component spaces. This is used to show that the inf map (a,b) → a ⊓ b on a complete lattice is continuous. The motivation for introducing the lower topology to mathlib is that, along with the Scott Topology (topology.omega_complete_partial_order) it is used to define the Lawson topology (Gierz et al, Chapter III).