Commit 2026-04-28 14:27 f6f458a4

View on Github →

chore(Topology): redefine TopologicalSpace.Opens.mapMapIso using OrderIso.equivalence (#38178) This was a TODO.

Estimated changes

Modified Mathlib/Topology/Category/TopCat/Opens.lean

modified def TopologicalSpace.Opens.mapMapIso

added theorem TopologicalSpace.Opens.mapMapIso_counitIso

added theorem TopologicalSpace.Opens.mapMapIso_functor

added theorem TopologicalSpace.Opens.mapMapIso_inverse

added theorem TopologicalSpace.Opens.mapMapIso_unitIso