mathlib

38fe3f3c - feat(topology/order/lower_topology): Introduce the lower topology on a preorder (#17426)

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).