mathlib3

24e3b5f5 - refactor(topology/opens): Turn `opens.gi` into a Galois coinsertion (#12547)

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 α`.