Commit 2025-10-29 00:35 e590bd91

View on Github →

feat(Topology/Sheaves): the equivalence Over U ≌ Opens U for U : Opens X (#30415)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Sheaves/Over.lean

added def TopologicalSpace.Opens.overEquivalence