Lattice

📁 Source: Mathlib/CategoryTheory/Limits/Lattice.lean

Statistics

Metric	Count
Definitions `colimitCocone`, `finiteColimitCocone`, `finiteLimitCone`, `limitCone`	4
Theorems `colimitCocone_cocone_pt`, `colimitCocone_cocone_ι_app`, `colimitCocone_isColimit_desc`, `colimit_eq_iSup`, `coprod_eq_sup`, `finiteColimitCocone_cocone_pt`, `finiteColimitCocone_cocone_ι_app`, `finiteColimitCocone_isColimit_desc`, `finiteLimitCone_cone_pt`, `finiteLimitCone_cone_π_app`, `finiteLimitCone_isLimit_lift`, `finite_colimit_eq_finset_univ_sup`, `finite_coproduct_eq_finset_sup`, `finite_limit_eq_finset_univ_inf`, `finite_product_eq_finset_inf`, `hasColimits_of_completeLattice`, `hasFiniteColimits_of_semilatticeSup_orderBot`, `hasFiniteLimits_of_semilatticeInf_orderTop`, `hasLimits_of_completeLattice`, `instHasBinaryCoproductsOfOrderBot`, `instHasBinaryProductsOfOrderTop`, `limitCone_cone_pt`, `limitCone_cone_π_app`, `limitCone_isLimit_lift`, `limit_eq_iInf`, `prod_eq_inf`, `pullback_eq_inf`, `pushout_eq_sup`	28
Total	32

CategoryTheory.Limits.CompleteLattice

Definitions

Name	Category	Theorems
`colimitCocone` 📖	CompOp	3 math math: `colimitCocone_cocone_pt`, `colimitCocone_cocone_ι_app`, `colimitCocone_isColimit_desc`
`finiteColimitCocone` 📖	CompOp	3 math math: `finiteColimitCocone_cocone_ι_app`, `finiteColimitCocone_cocone_pt`, `finiteColimitCocone_isColimit_desc`
`finiteLimitCone` 📖	CompOp	3 math math: `finiteLimitCone_isLimit_lift`, `finiteLimitCone_cone_pt`, `finiteLimitCone_cone_π_app`
`limitCone` 📖	CompOp	3 math math: `limitCone_isLimit_lift`, `limitCone_cone_π_app`, `limitCone_cone_pt`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`colimitCocone_cocone_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cocone.pt` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CategoryTheory.Limits.ColimitCocone.cocone` `colimitCocone` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `CategoryTheory.Functor.obj`	—	—
`colimitCocone_cocone_ι_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `CategoryTheory.Limits.Cocone.ι` `CategoryTheory.Limits.ColimitCocone.cocone` `colimitCocone` `CategoryTheory.homOfLE`	—	—
`colimitCocone_isColimit_desc` 📖	mathematical	—	`CategoryTheory.Limits.IsColimit.desc` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.homOfLE` `CategoryTheory.Limits.ColimitCocone.isColimit` `colimitCocone` `CategoryTheory.Limits.Cocone.pt`	—	—
`colimit_eq_iSup` 📖	mathematical	—	`CategoryTheory.Limits.colimit` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize` `hasColimits_of_completeLattice` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `CategoryTheory.Functor.obj`	—	`CategoryTheory.Iso.to_eq` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize` `hasColimits_of_completeLattice`
`coprod_eq_sup` 📖	mathematical	—	`CategoryTheory.Limits.coprod` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `instHasBinaryCoproductsOfOrderBot` `CategoryTheory.Limits.pair` `SemilatticeSup.toMax`	—	`CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `instHasBinaryCoproductsOfOrderBot` `CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits` `hasFiniteColimits_of_semilatticeSup_orderBot` `finite_colimit_eq_finset_univ_sup` `sup_bot_eq`
`finiteColimitCocone_cocone_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cocone.pt` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `CategoryTheory.Limits.ColimitCocone.cocone` `finiteColimitCocone` `Finset.sup` `Finset.univ` `CategoryTheory.FinCategory.fintypeObj` `CategoryTheory.Functor.obj`	—	—
`finiteColimitCocone_cocone_ι_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `Finset.sup` `Finset.univ` `CategoryTheory.FinCategory.fintypeObj` `CategoryTheory.Limits.Cocone.ι` `CategoryTheory.Limits.ColimitCocone.cocone` `finiteColimitCocone` `CategoryTheory.homOfLE`	—	—
`finiteColimitCocone_isColimit_desc` 📖	mathematical	—	`CategoryTheory.Limits.IsColimit.desc` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Finset.sup` `Finset.univ` `CategoryTheory.FinCategory.fintypeObj` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.homOfLE` `CategoryTheory.Limits.ColimitCocone.isColimit` `finiteColimitCocone` `CategoryTheory.Limits.Cocone.pt`	—	—
`finiteLimitCone_cone_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cone.pt` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `CategoryTheory.Limits.LimitCone.cone` `finiteLimitCone` `Finset.inf` `Finset.univ` `CategoryTheory.FinCategory.fintypeObj` `CategoryTheory.Functor.obj`	—	—
`finiteLimitCone_cone_π_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `Finset.inf` `Finset.univ` `CategoryTheory.FinCategory.fintypeObj` `CategoryTheory.Limits.Cone.π` `CategoryTheory.Limits.LimitCone.cone` `finiteLimitCone` `CategoryTheory.homOfLE`	—	—
`finiteLimitCone_isLimit_lift` 📖	mathematical	—	`CategoryTheory.Limits.IsLimit.lift` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Finset.inf` `Finset.univ` `CategoryTheory.FinCategory.fintypeObj` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.homOfLE` `CategoryTheory.Limits.LimitCone.isLimit` `finiteLimitCone` `CategoryTheory.Limits.Cone.pt`	—	—
`finite_colimit_eq_finset_univ_sup` 📖	mathematical	—	`CategoryTheory.Limits.colimit` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits` `hasFiniteColimits_of_semilatticeSup_orderBot` `Finset.sup` `Finset.univ` `CategoryTheory.FinCategory.fintypeObj` `CategoryTheory.Functor.obj`	—	`CategoryTheory.Iso.to_eq` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits` `hasFiniteColimits_of_semilatticeSup_orderBot`
`finite_coproduct_eq_finset_sup` 📖	mathematical	—	`CategoryTheory.Limits.sigmaObj` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits` `hasFiniteColimits_of_semilatticeSup_orderBot` `CategoryTheory.finCategoryDiscreteOfFintype` `CategoryTheory.Discrete.functor` `Finset.sup` `Fintype.elems`	—	`CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits` `hasFiniteColimits_of_semilatticeSup_orderBot` `CategoryTheory.Iso.to_eq` `Finset.univ_map_equiv_to_embedding`
`finite_limit_eq_finset_univ_inf` 📖	mathematical	—	`CategoryTheory.Limits.limit` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits` `hasFiniteLimits_of_semilatticeInf_orderTop` `Finset.inf` `Finset.univ` `CategoryTheory.FinCategory.fintypeObj` `CategoryTheory.Functor.obj`	—	`CategoryTheory.Iso.to_eq` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits` `hasFiniteLimits_of_semilatticeInf_orderTop`
`finite_product_eq_finset_inf` 📖	mathematical	—	`CategoryTheory.Limits.piObj` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits` `hasFiniteLimits_of_semilatticeInf_orderTop` `CategoryTheory.finCategoryDiscreteOfFintype` `CategoryTheory.Discrete.functor` `Finset.inf` `Fintype.elems`	—	`CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits` `hasFiniteLimits_of_semilatticeInf_orderTop` `CategoryTheory.Iso.to_eq` `Finset.univ_map_equiv_to_embedding`
`hasColimits_of_completeLattice` 📖	mathematical	—	`CategoryTheory.Limits.HasColimitsOfSize` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf`	—	—
`hasFiniteColimits_of_semilatticeSup_orderBot` 📖	mathematical	—	`CategoryTheory.Limits.HasFiniteColimits` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	—	—
`hasFiniteLimits_of_semilatticeInf_orderTop` 📖	mathematical	—	`CategoryTheory.Limits.HasFiniteLimits` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	—	—
`hasLimits_of_completeLattice` 📖	mathematical	—	`CategoryTheory.Limits.HasLimitsOfSize` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf`	—	—
`instHasBinaryCoproductsOfOrderBot` 📖	mathematical	—	`CategoryTheory.Limits.HasBinaryCoproducts` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	—	`CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits` `hasFiniteColimits_of_semilatticeSup_orderBot` `CategoryTheory.Limits.hasBinaryCoproducts_of_hasColimit_pair`
`instHasBinaryProductsOfOrderTop` 📖	mathematical	—	`CategoryTheory.Limits.HasBinaryProducts` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	—	`CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits` `hasFiniteLimits_of_semilatticeInf_orderTop` `CategoryTheory.Limits.hasBinaryProducts_of_hasLimit_pair`
`limitCone_cone_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cone.pt` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CategoryTheory.Limits.LimitCone.cone` `limitCone` `iInf` `CompleteSemilatticeInf.toInfSet` `CategoryTheory.Functor.obj`	—	—
`limitCone_cone_π_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `iInf` `CompleteSemilatticeInf.toInfSet` `CategoryTheory.Limits.Cone.π` `CategoryTheory.Limits.LimitCone.cone` `limitCone` `CategoryTheory.homOfLE`	—	—
`limitCone_isLimit_lift` 📖	mathematical	—	`CategoryTheory.Limits.IsLimit.lift` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `iInf` `CompleteSemilatticeInf.toInfSet` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.homOfLE` `CategoryTheory.Limits.LimitCone.isLimit` `limitCone` `CategoryTheory.Limits.Cone.pt`	—	—
`limit_eq_iInf` 📖	mathematical	—	`CategoryTheory.Limits.limit` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits` `hasLimits_of_completeLattice` `iInf` `CompleteSemilatticeInf.toInfSet` `CategoryTheory.Functor.obj`	—	`CategoryTheory.Iso.to_eq` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits` `hasLimits_of_completeLattice`
`prod_eq_inf` 📖	mathematical	—	`CategoryTheory.Limits.prod` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `instHasBinaryProductsOfOrderTop` `CategoryTheory.Limits.pair` `SemilatticeInf.toMin`	—	`CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `instHasBinaryProductsOfOrderTop` `CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits` `hasFiniteLimits_of_semilatticeInf_orderTop` `finite_limit_eq_finset_univ_inf` `inf_top_eq`
`pullback_eq_inf` 📖	mathematical	—	`CategoryTheory.Limits.pullback` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `hasFiniteLimits_of_semilatticeInf_orderTop` `CategoryTheory.Limits.cospan` `SemilatticeInf.toMin`	—	`CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `hasFiniteLimits_of_semilatticeInf_orderTop` `CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits` `finite_limit_eq_finset_univ_inf` `inf_top_eq` `inf_eq_right` `inf_le_of_left_le`
`pushout_eq_sup` 📖	mathematical	—	`CategoryTheory.Limits.pushout` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.WalkingSpan` `CategoryTheory.Limits.WidePushoutShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits` `hasFiniteColimits_of_semilatticeSup_orderBot` `CategoryTheory.Limits.span` `SemilatticeSup.toMax`	—	`CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits` `hasFiniteColimits_of_semilatticeSup_orderBot` `CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits` `finite_colimit_eq_finset_univ_sup` `sup_bot_eq` `sup_eq_right` `le_sup_of_le_left`

---

← Back to Index