Def TopologicalSpace.Opens.overEquivalence

Modification history

2025-10-29 00:35
Mathlib/Topology/Sheaves/Over.lean
feat(Topology/Sheaves): the equivalence `Over U ≌ Opens U` for `U : Opens X` (#30415)
Added TopologicalSpace.Opens.overEquivalenceView on Github →