Over

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

Statistics

Metric	Count
Definitions overPost	1
Theorems instGuitartExactOverObjOverPostOfHasBinaryProductOfPreservesLimitDiscreteWalkingPairPair	1
Total	2

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instGuitartExactOverObjOverPostOfHasBinaryProductOfPreservesLimitDiscreteWalkingPairPair 📖	mathematical	Limits.HasBinaryProduct Limits.PreservesLimit Discrete Limits.WalkingPair discreteCategory Limits.pair	TwoSquare.GuitartExact Over Functor.obj instCategoryOver Over.post Over.forget TwoSquare.overPost	—	Limits.instHasBinaryProductObjOfPreservesLimitDiscreteWalkingPairPair Limits.instIsIsoProdComparison Category.assoc Limits.inv_prodComparison_map_fst Limits.limit.lift_π Category.id_comp Limits.inv_prodComparison_map_snd CostructuredArrow.hom_ext Over.OverMorphism.ext cancel_mono mono_of_strongMono strongMono_of_isIso Limits.prod.hom_ext Limits.prodComparison_fst IsIso.inv_hom_id Category.comp_id Over.w Limits.prodComparison_snd CostructuredArrow.w zigzag_isConnected Zigzag.trans Zigzag.of_hom Zigzag.of_inv

CategoryTheory.TwoSquare

Definitions

Name	Category	Theorems
overPost 📖	CompOp	1 math math: CategoryTheory.instGuitartExactOverObjOverPostOfHasBinaryProductOfPreservesLimitDiscreteWalkingPairPair

---

← Back to Index