Def TopologicalSpace.Opens.mapMapIso

Modification history

2026-04-28 14:27

Mathlib/Topology/Category/TopCat/Opens.lean

chore(Topology): redefine TopologicalSpace.Opens.mapMapIso using OrderIso.equivalence (#38178) …

Modified TopologicalSpace.Opens.mapMapIso View on Github →

2023-04-27 02:37

Mathlib/Topology/Category/Top/Opens.lean

feat: port Topology.Category.Top.Opens (#3662)

Added TopologicalSpace.Opens.mapMapIso View on Github →