InfSemilattice

📁 Source: Mathlib/CategoryTheory/Monoidal/Cartesian/InfSemilattice.lean

Statistics

Metric	Count
Definitions braidedCategory, cartesianMonoidalCategory	2
Theorems tensorObj, tensorUnit	2
Total	4

CategoryTheory.SemilatticeInf

Definitions

Name	Category	Theorems
braidedCategory 📖	CompOp	—
cartesianMonoidalCategory 📖	CompOp	2 math math: tensorUnit, tensorObj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tensorObj 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorObj Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory SemilatticeInf.toMin	—	—
tensorUnit 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorUnit Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory Top.top OrderTop.toTop Preorder.toLE	—	—

---

← Back to Index