Commit 2024-07-16 22:20 c2bcd261

View on Github →

refactor(Topology/Category): refactor CompHaus.Basic (#13908) This PR refactors the file CompHaus.Basic in terms of the new CompHausLike API. Other files are touched only to fix errors created by this refactor, they will be refactored later (in particular, the API for explicit limits will be mostly removed in favour of the general API for explicit limits in CompHausLike, see #12930).

Estimated changes

Modified Mathlib/Condensed/TopCatAdjunction.lean

Modified Mathlib/Topology/Category/CompHaus/Basic.lean

deleted theorem CompHaus.coe_of

deleted def CompHaus.homeoOfIso

deleted theorem CompHaus.isClosedMap

deleted theorem CompHaus.isIso_of_bijective

deleted def CompHaus.isoEquivHomeo

deleted def CompHaus.isoOfHomeo

deleted theorem CompHaus.mono_iff_injective

deleted def CompHaus.of

deleted structure CompHaus

deleted def compHausToTop

Modified Mathlib/Topology/Category/CompHaus/Limits.lean

Modified Mathlib/Topology/Category/Compactum.lean

Modified Mathlib/Topology/Category/LightProfinite/Basic.lean

modified def LightProfinite.homeoOfIso

Modified Mathlib/Topology/Category/Profinite/Basic.lean

modified def Profinite.homeoOfIso

Modified Mathlib/Topology/Category/Stonean/Basic.lean

modified def Stonean.homeoOfIso

Modified Mathlib/Topology/Category/Stonean/Limits.lean