Basic

📁 Source: Mathlib/Topology/Category/TopCat/Limits/Basic.lean

Statistics

Metric	Count
Definitions `coconeOfCoconeForget`, `coconePtOfCoconeForget`, `coneOfConeForget`, `conePtOfConeForget`, `initialIsoPEmpty`, `isColimitCoconeOfForget`, `isInitialPEmpty`, `isLimitConeOfForget`, `isTerminalPUnit`, `limitCone`, `limitConeIsLimit`, `terminalIsoPUnit`, `topologicalSpaceCoconePtOfCoconeForget`, `topologicalSpaceConePtOfConeForget`	14
Theorems `coconeOfCoconeForget_pt`, `coconeOfCoconeForget_ι_app`, `coinduced_of_isColimit`, `colimit_isOpen_iff`, `colimit_topology`, `coneOfConeForget_pt`, `coneOfConeForget_π_app`, `continuous_iff_of_isColimit`, `forget_preservesColimits`, `forget_preservesColimitsOfSize`, `forget_preservesLimits`, `forget_preservesLimitsOfSize`, `hasColimit_iff_small_colimitType`, `hasLimit_iff_small_sections`, `induced_of_isLimit`, `isClosed_iff_of_isColimit`, `isOpen_iff_of_isColimit`, `limit_topology`, `nonempty_isColimit_iff_eq_coinduced`, `nonempty_isLimit_iff_eq_induced`, `topCat_hasColimits`, `topCat_hasColimitsOfShape`, `topCat_hasColimitsOfSize`, `topCat_hasLimits`, `topCat_hasLimitsOfShape`, `topCat_hasLimitsOfSize`	26
Total	40

TopCat

Definitions

Name	Category	Theorems
`coconeOfCoconeForget` 📖	CompOp	2 math math: `coconeOfCoconeForget_pt`, `coconeOfCoconeForget_ι_app`
`coconePtOfCoconeForget` 📖	CompOp	2 math math: `coconeOfCoconeForget_pt`, `coconeOfCoconeForget_ι_app`
`coneOfConeForget` 📖	CompOp	2 math math: `coneOfConeForget_π_app`, `coneOfConeForget_pt`
`conePtOfConeForget` 📖	CompOp	2 math math: `coneOfConeForget_π_app`, `coneOfConeForget_pt`
`initialIsoPEmpty` 📖	CompOp	—
`isColimitCoconeOfForget` 📖	CompOp	—
`isInitialPEmpty` 📖	CompOp	—
`isLimitConeOfForget` 📖	CompOp	—
`isTerminalPUnit` 📖	CompOp	—
`limitCone` 📖	CompOp	1 math math: `nonempty_limitCone_of_compact_t2_cofiltered_system`
`limitConeIsLimit` 📖	CompOp	—
`terminalIsoPUnit` 📖	CompOp	—
`topologicalSpaceCoconePtOfCoconeForget` 📖	CompOp	2 math math: `coconeOfCoconeForget_pt`, `coconeOfCoconeForget_ι_app`
`topologicalSpaceConePtOfConeForget` 📖	CompOp	2 math math: `coneOfConeForget_π_app`, `coneOfConeForget_pt`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coconeOfCoconeForget_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cocone.pt` `TopCat` `instCategory` `coconeOfCoconeForget` `of` `coconePtOfCoconeForget` `topologicalSpaceCoconePtOfCoconeForget`	—	—
`coconeOfCoconeForget_ι_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `TopCat` `instCategory` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `of` `coconePtOfCoconeForget` `topologicalSpaceCoconePtOfCoconeForget` `CategoryTheory.Limits.Cocone.ι` `coconeOfCoconeForget` `ofHom` `carrier` `str` `CategoryTheory.types` `CategoryTheory.Functor.comp` `CategoryTheory.forget` `ContinuousMap` `ContinuousMap.instFunLike` `instConcreteCategoryContinuousMapCarrier` `CategoryTheory.Limits.Cocone.pt`	—	—
`coinduced_of_isColimit` 📖	mathematical	—	`str` `CategoryTheory.Limits.Cocone.pt` `TopCat` `instCategory` `iSup` `TopologicalSpace` `carrier` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.instCompleteLattice` `TopologicalSpace.coinduced` `CategoryTheory.Functor.obj` `DFunLike.coe` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.ConcreteCategory.hom` `ContinuousMap` `ContinuousMap.instFunLike` `instConcreteCategoryContinuousMapCarrier` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι`	—	`CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit` `CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `instIsLeftAdjointForgetContinuousMapCarrier` `CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom` `Homeomorph.coinduced_eq` `coinduced_iSup`
`colimit_isOpen_iff` 📖	mathematical	—	`IsOpen` `carrier` `CategoryTheory.Limits.colimit` `TopCat` `instCategory` `str` `CategoryTheory.Functor.obj` `Set.preimage` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `ContinuousMap` `ContinuousMap.instFunLike` `instConcreteCategoryContinuousMapCarrier` `CategoryTheory.Limits.colimit.ι`	—	`isOpen_iff_of_isColimit`
`colimit_topology` 📖	mathematical	—	`str` `CategoryTheory.Limits.colimit` `TopCat` `instCategory` `iSup` `TopologicalSpace` `carrier` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.instCompleteLattice` `TopologicalSpace.coinduced` `CategoryTheory.Functor.obj` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `ContinuousMap` `ContinuousMap.instFunLike` `instConcreteCategoryContinuousMapCarrier` `CategoryTheory.Limits.colimit.ι`	—	`coinduced_of_isColimit`
`coneOfConeForget_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cone.pt` `TopCat` `instCategory` `coneOfConeForget` `of` `conePtOfConeForget` `topologicalSpaceConePtOfConeForget`	—	—
`coneOfConeForget_π_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `TopCat` `instCategory` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `of` `conePtOfConeForget` `topologicalSpaceConePtOfConeForget` `CategoryTheory.Limits.Cone.π` `coneOfConeForget` `ofHom` `carrier` `str` `CategoryTheory.types` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Functor.comp` `CategoryTheory.forget` `ContinuousMap` `ContinuousMap.instFunLike` `instConcreteCategoryContinuousMapCarrier`	—	—
`continuous_iff_of_isColimit` 📖	mathematical	—	`Continuous` `carrier` `CategoryTheory.Limits.Cocone.pt` `TopCat` `instCategory` `str` `CategoryTheory.Functor.obj` `DFunLike.coe` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.ConcreteCategory.hom` `ContinuousMap` `ContinuousMap.instFunLike` `instConcreteCategoryContinuousMapCarrier` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι`	—	`isOpen_iff_of_isColimit`
`forget_preservesColimits` 📖	mathematical	—	`CategoryTheory.Limits.PreservesColimits` `TopCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `ContinuousMap` `carrier` `str` `ContinuousMap.instFunLike` `instConcreteCategoryContinuousMapCarrier`	—	`CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `instIsLeftAdjointForgetContinuousMapCarrier`
`forget_preservesColimitsOfSize` 📖	mathematical	—	`CategoryTheory.Limits.PreservesColimitsOfSize` `TopCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `ContinuousMap` `carrier` `str` `ContinuousMap.instFunLike` `instConcreteCategoryContinuousMapCarrier`	—	`CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `instIsLeftAdjointForgetContinuousMapCarrier`
`forget_preservesLimits` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimits` `TopCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `ContinuousMap` `carrier` `str` `ContinuousMap.instFunLike` `instConcreteCategoryContinuousMapCarrier`	—	`CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint` `instIsRightAdjointForgetContinuousMapCarrier`
`forget_preservesLimitsOfSize` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimitsOfSize` `TopCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `ContinuousMap` `carrier` `str` `ContinuousMap.instFunLike` `instConcreteCategoryContinuousMapCarrier`	—	`CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint` `instIsRightAdjointForgetContinuousMapCarrier`
`hasColimit_iff_small_colimitType` 📖	mathematical	—	`CategoryTheory.Limits.HasColimit` `TopCat` `instCategory` `Small` `CategoryTheory.Functor.ColimitType` `CategoryTheory.Functor.comp` `CategoryTheory.types` `CategoryTheory.forget` `ContinuousMap` `carrier` `str` `ContinuousMap.instFunLike` `instConcreteCategoryContinuousMapCarrier`	—	`CategoryTheory.Limits.Types.hasColimit_iff_small_colimitType` `CategoryTheory.Limits.instHasColimitCompOfPreservesColimit` `CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit` `CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `instIsLeftAdjointForgetContinuousMapCarrier`
`hasLimit_iff_small_sections` 📖	mathematical	—	`CategoryTheory.Limits.HasLimit` `TopCat` `instCategory` `Small` `Set.Elem` `CategoryTheory.Functor.sections` `CategoryTheory.Functor.comp` `CategoryTheory.types` `CategoryTheory.forget` `ContinuousMap` `carrier` `str` `ContinuousMap.instFunLike` `instConcreteCategoryContinuousMapCarrier`	—	`CategoryTheory.Limits.Types.hasLimit_iff_small_sections` `CategoryTheory.Limits.instHasLimitCompOfPreservesLimit` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint` `instIsRightAdjointForgetContinuousMapCarrier`
`induced_of_isLimit` 📖	mathematical	—	`str` `CategoryTheory.Limits.Cone.pt` `TopCat` `instCategory` `iInf` `TopologicalSpace` `carrier` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.instCompleteLattice` `TopologicalSpace.induced` `CategoryTheory.Functor.obj` `DFunLike.coe` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.ConcreteCategory.hom` `ContinuousMap` `ContinuousMap.instFunLike` `instConcreteCategoryContinuousMapCarrier` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cone.π`	—	`CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint` `instIsRightAdjointForgetContinuousMapCarrier` `CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp` `Homeomorph.induced_eq` `induced_iInf`
`isClosed_iff_of_isColimit` 📖	mathematical	—	`IsClosed` `carrier` `CategoryTheory.Limits.Cocone.pt` `TopCat` `instCategory` `str` `CategoryTheory.Functor.obj` `Set.preimage` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `ContinuousMap` `ContinuousMap.instFunLike` `instConcreteCategoryContinuousMapCarrier` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι`	—	`isOpen_iff_of_isColimit`
`isOpen_iff_of_isColimit` 📖	mathematical	—	`IsOpen` `carrier` `CategoryTheory.Limits.Cocone.pt` `TopCat` `instCategory` `str` `CategoryTheory.Functor.obj` `Set.preimage` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `ContinuousMap` `ContinuousMap.instFunLike` `instConcreteCategoryContinuousMapCarrier` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι`	—	`coinduced_of_isColimit` `isOpen_fold` `isOpen_iSup_iff`
`limit_topology` 📖	mathematical	—	`str` `CategoryTheory.Limits.limit` `TopCat` `instCategory` `iInf` `TopologicalSpace` `carrier` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.instCompleteLattice` `TopologicalSpace.induced` `CategoryTheory.Functor.obj` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `ContinuousMap` `ContinuousMap.instFunLike` `instConcreteCategoryContinuousMapCarrier` `CategoryTheory.Limits.limit.π`	—	`induced_of_isLimit`
`nonempty_isColimit_iff_eq_coinduced` 📖	mathematical	—	`CategoryTheory.Limits.IsColimit` `TopCat` `instCategory` `str` `CategoryTheory.Limits.Cocone.pt` `iSup` `TopologicalSpace` `carrier` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.instCompleteLattice` `TopologicalSpace.coinduced` `CategoryTheory.Functor.obj` `DFunLike.coe` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.ConcreteCategory.hom` `ContinuousMap` `ContinuousMap.instFunLike` `instConcreteCategoryContinuousMapCarrier` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι`	—	`coinduced_of_isColimit` `continuous_id'`
`nonempty_isLimit_iff_eq_induced` 📖	mathematical	—	`CategoryTheory.Limits.IsLimit` `TopCat` `instCategory` `str` `CategoryTheory.Limits.Cone.pt` `iInf` `TopologicalSpace` `carrier` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.instCompleteLattice` `TopologicalSpace.induced` `CategoryTheory.Functor.obj` `DFunLike.coe` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.ConcreteCategory.hom` `ContinuousMap` `ContinuousMap.instFunLike` `instConcreteCategoryContinuousMapCarrier` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cone.π`	—	`induced_of_isLimit` `continuous_id'`
`topCat_hasColimits` 📖	mathematical	—	`CategoryTheory.Limits.HasColimits` `TopCat` `instCategory`	—	`topCat_hasColimitsOfSize` `UnivLE.self`
`topCat_hasColimitsOfShape` 📖	mathematical	—	`CategoryTheory.Limits.HasColimitsOfShape` `TopCat` `instCategory`	—	`hasColimit_iff_small_colimitType` `CategoryTheory.Functor.instSmallColimitType`
`topCat_hasColimitsOfSize` 📖	mathematical	—	`CategoryTheory.Limits.HasColimitsOfSize` `TopCat` `instCategory`	—	`topCat_hasColimitsOfShape` `UnivLE.small`
`topCat_hasLimits` 📖	mathematical	—	`CategoryTheory.Limits.HasLimits` `TopCat` `instCategory`	—	`topCat_hasLimitsOfSize` `UnivLE.self`
`topCat_hasLimitsOfShape` 📖	mathematical	—	`CategoryTheory.Limits.HasLimitsOfShape` `TopCat` `instCategory`	—	`hasLimit_iff_small_sections` `small_subtype` `small_Pi` `UnivLE.small` `UnivLE.self`
`topCat_hasLimitsOfSize` 📖	mathematical	—	`CategoryTheory.Limits.HasLimitsOfSize` `TopCat` `instCategory`	—	`topCat_hasLimitsOfShape` `UnivLE.small`

---

← Back to Index