mathlib

bab039fb - feat(topology/opens): The frame of opens of a topological space (#12546)

feat(topology/opens): The frame of opens of a topological space (#12546) Provide the `frame` instance for `opens α` and strengthen `opens.comap` from `order_hom` to `frame_hom`.