Commit 2024-07-30 16:32 e7b14b1e

View on Github →

refactor(Topology/Category): refactor Stonean.Basic (#13911) This is the second part of the refactor of CompHaus and friends (refactoring the definition of Stonean in terms of CompHausLike, see #12930 for the end result)

Estimated changes

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

deleted theorem Stonean.mono_iff_injective

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

modified def CompHaus.presentation.π

deleted def Stonean.fullyFaithfulToCompHaus

deleted def Stonean.homeoOfIso

deleted def Stonean.isoEquivHomeo

deleted def Stonean.isoOfHomeo

deleted def Stonean.of

deleted def Stonean.toCompHaus

deleted def Stonean.toProfinite

deleted structure Stonean

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

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