Commit 2022-03-10 07:37 24e3b5f5

refactor(topology/opens): Turn opens.gi into a Galois coinsertion (#12547) topological_space.opens.gi is currently a galois_insertion between order_dual (opens α) and order_dual (set α). This turns it into the sensible thing, namely a galois_coinsertion between opens α and set α.