Over

📁 Source: Mathlib/CategoryTheory/LiftingProperties/Over.lean

Statistics

Metric	Count
Definitions	0
Theorems over, over	2
Total	2

CategoryTheory.CommSq.HasLift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
over 📖	mathematical	CategoryTheory.CommSq CategoryTheory.Over CategoryTheory.instCategoryOver	CategoryTheory.CommSq.HasLift	—	CategoryTheory.CommSq.map CategoryTheory.Over.w CategoryTheory.CommSq.fac_right_assoc CategoryTheory.Over.OverMorphism.ext CategoryTheory.CommSq.fac_left CategoryTheory.CommSq.fac_right

CategoryTheory.HasLiftingProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
over 📖	mathematical	—	CategoryTheory.HasLiftingProperty CategoryTheory.Over CategoryTheory.instCategoryOver	—	CategoryTheory.CommSq.HasLift.over CategoryTheory.sq_hasLift_of_hasLiftingProperty CategoryTheory.CommSq.map

---

← Back to Index