mathlib

60851c93 - feat(topology/order/lattice): add `topological_lattice` instance for linear orders with an order closed topology (#16664)

feat(topology/order/lattice): add `topological_lattice` instance for linear orders with an order closed topology (#16664) This adds a `topological_lattice` instance for and linear order with an order closed topology. In particular, this gives us previously nonexistent `topological_lattice` instances for `ℝ≥0`, `ℝ≥0∞` and things like `set.Icc (a : ℝ) b` as well as many others. In addition, it makes the `topological_lattice` instance for `ℝ` available earlier in the import hierarchy, because the previously existing instance was derived from `real.normed_lattice_add_comm_group` via `normed_lattice_add_comm_group_topological_lattice`.