Commit 2025-03-04 22:56 55c288c4

View on Github →

chore(Topology/Category): generalize topCat_hasLimitsOfSize to more universes (#22540) And the same for topCat_hasColimitsOfSize.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Category/TopCat/Limits/Basic.lean

added def TopCat.coneOfConeForget

added def TopCat.conePtOfConeForget

added theorem TopCat.hasLimit_iff_small_sections

added theorem TopCat.induced_of_isLimit

added def TopCat.isLimitConeOfForget

deleted def TopCat.limitConeInfi

deleted def TopCat.limitConeInfiIsLimit

added theorem TopCat.limit_topology

Modified Mathlib/Topology/Category/TopCat/Limits/Cofiltered.lean

Modified Mathlib/Topology/Category/TopCat/Limits/Products.lean

deleted theorem TopCat.induced_of_isLimit

deleted theorem TopCat.limit_topology

Created Mathlib/Topology/Instances/Shrink.lean