refactor(Topology/Category): refactor Stonean.Basic

[dagurtomas]

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)

---

• [x] depends on: #13904
• [x] depends on: #13905
• [x] depends on: #13907
• [ ] depends on: #13908
• [ ] depends on: #13909

[github-actions[bot]]

PR summary 5f49bf0cbc

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ instance (X : Stonean.{u}) : ExtremallyDisconnected ((forget _).obj X) := X.prop + instance (X : Stonean.{u}) : ExtremallyDisconnected X := X.prop + instance (X : Stonean.{u}) : TotallyDisconnectedSpace ((forget _).obj X) + instance (X : Type*) [TopologicalSpace X] - Stonean - fullyFaithfulToCompHaus - homeoOfIso - instTopologicalSpace - instance (X : Stonean.{u}) : CompactSpace X - instance (X : Stonean.{u}) : ExtremallyDisconnected X - instance (X : Stonean.{u}) : T2Space X - instance : CoeSort Stonean.{u} (Type u) := ConcreteCategory.hasCoeToSort _ - instance : ConcreteCategory Stonean - instance : LargeCategory Stonean.{u} - instance : toCompHaus.Faithful := fullyFaithfulToCompHaus.faithful - instance : toCompHaus.Full := fullyFaithfulToCompHaus.full - instance : toProfinite.Faithful := {} - instance : toProfinite.Full - instance {X Y : Stonean.{u}} : FunLike (X ⟶ Y) X Y := ConcreteCategory.instFunLike - instance {X Y : Stonean} (f : X ⟶ Y) [@Epi CompHaus _ _ _ f] : Epi f := by - instance {X Y : Stonean} (f : X ⟶ Y) [Epi f] : @Epi CompHaus _ _ _ f := by - isoEquivHomeo - isoOfHomeo - mono_iff_injective - of - toCompHaus - toProfinite

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#13904~~
• ~~leanprover-community/mathlib4#13905~~
• ~~leanprover-community/mathlib4#13907~~
• ~~leanprover-community/mathlib4#13908~~
• ~~leanprover-community/mathlib4#13909~~ By Dependent Issues (🤖). Happy coding!

[joelriou]

Thanks!

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style