Commit 2023-04-27 14:06 1c05ad40

View on Github →

feat: port Topology.Category.Top.Limits.Basic (#3487)

Estimated changes

Modified Mathlib.lean

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

Created Mathlib/Topology/Category/Top/Limits/Basic.lean

added def TopCat.colimitCocone

added def TopCat.colimitCoconeIsColimit

added def TopCat.limitCone

added def TopCat.limitConeInfi

added def TopCat.limitConeInfiIsLimit

added def TopCat.limitConeIsLimit