Theorem TopologicalSpace.Opens.mapMapIso_counitIso

Modification history

2026-05-01 00:39

Mathlib/Topology/Category/TopCat/Opens.lean

chore(Topology/Category): replace `TopCat` by `TopCat.{u}` (#38779) …

Modified TopologicalSpace.Opens.mapMapIso_counitIso View on Github →

2026-04-28 14:27

Mathlib/Topology/Category/TopCat/Opens.lean

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

Added TopologicalSpace.Opens.mapMapIso_counitIso View on Github →