Commit 2021-09-08 12:15 57a0789b

chore(topology/order): relate Sup and Inf of topologies to generate_from (#9045) Since there is a Galois insertion between generate_from : set (set α) → topological_space α and the "forgetful functor" topological_space α → set (set α), all kinds of lemmas about the interaction of generate_from and the ordering on topologies automatically follow. But it is hard to use the Galois insertion lemmas directly, because the Galois insertion is actually provided for the dual order on topologies, which confuses Lean. Here we re-state most of the Galois insertion API in this special case.