Commit 2024-05-02 22:40 437c7c8b

View on Github →

chore(Topology/Category): remove ProfiniteMax and CompHausMax (#12599) They are no longer necessary after [#3981](https://github.com/leanprover/lean4/pull/3981)

Estimated changes

modified def Profinite.limitCone
modified def TopCat.colimitCocone
modified def TopCat.limitCone
modified def TopCat.limitConeInfi
modified theorem TopCat.induced_of_isLimit
modified theorem TopCat.limit_topology
modified def TopCat.piFan
modified def TopCat.piFanIsLimit
modified def TopCat.piIsoPi
modified theorem TopCat.piIsoPi_hom_apply
modified theorem TopCat.piIsoPi_inv_π
modified theorem TopCat.piIsoPi_inv_π_apply
modified def TopCat.sigmaCofan
modified def TopCat.sigmaIsoSigma
modified theorem TopCat.sigmaIsoSigma_hom_ι
modified theorem TopCat.colimit_isOpen_iff
modified theorem TopCat.colimit_topology