OmegaCompletePartialOrder

📁 Source: Mathlib/Order/Category/OmegaCompletePartialOrder.lean

Statistics

Metric	Count
Definitions ωCPO, equalizer, equalizerι, isEqualizer, isProduct, product, carrier, instCoeSortType, instConcreteCategoryContinuousHomCarrier, instInhabited, instLargeCategory, omegaCompletePartialOrderEqualizer, str	13
Theorems instHasProduct, coe_of, instHasEqualizers, instHasLimitWalkingParallelPairParallelPair, instHasLimits, instHasProducts	6
Total	19

(root)

Definitions

Name	Category	Theorems
ωCPO 📖	CompData	5 math math: ωCPO.instHasProducts, ωCPO.instHasLimitWalkingParallelPairParallelPair, ωCPO.HasProducts.instHasProduct, ωCPO.instHasLimits, ωCPO.instHasEqualizers

ωCPO

Definitions

Name	Category	Theorems
carrier 📖	CompOp	1 math math: coe_of
instCoeSortType 📖	CompOp	—
instConcreteCategoryContinuousHomCarrier 📖	CompOp	—
instInhabited 📖	CompOp	—
instLargeCategory 📖	CompOp	5 math math: instHasProducts, instHasLimitWalkingParallelPairParallelPair, HasProducts.instHasProduct, instHasLimits, instHasEqualizers
omegaCompletePartialOrderEqualizer 📖	CompOp	—
str 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_of 📖	mathematical	—	carrier of	—	—
instHasEqualizers 📖	mathematical	—	CategoryTheory.Limits.HasEqualizers ωCPO instLargeCategory	—	CategoryTheory.Limits.hasEqualizers_of_hasLimit_parallelPair instHasLimitWalkingParallelPairParallelPair
instHasLimitWalkingParallelPairParallelPair 📖	mathematical	—	CategoryTheory.Limits.HasLimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory ωCPO instLargeCategory CategoryTheory.Limits.parallelPair	—	—
instHasLimits 📖	mathematical	—	CategoryTheory.Limits.HasLimits ωCPO instLargeCategory	—	CategoryTheory.Limits.has_limits_of_hasEqualizers_and_products instHasProducts instHasEqualizers
instHasProducts 📖	mathematical	—	CategoryTheory.Limits.HasProducts ωCPO instLargeCategory	—	CategoryTheory.Limits.hasLimit_of_iso HasProducts.instHasProduct

ωCPO.HasEqualizers

Definitions

Name	Category	Theorems
equalizer 📖	CompOp	—
equalizerι 📖	CompOp	—
isEqualizer 📖	CompOp	—

ωCPO.HasProducts

Definitions

Name	Category	Theorems
isProduct 📖	CompOp	—
product 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasProduct 📖	mathematical	—	CategoryTheory.Limits.HasProduct ωCPO ωCPO.instLargeCategory	—	—

---

← Back to Index