Commit 2022-03-10 05:29 bab039fb
View on Github →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.
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.