TruncLEGT

📁 Source: Mathlib/CategoryTheory/Triangulated/TStructure/TruncLEGT.lean

Statistics

Metric	Count
Definitions descTruncGT, liftTruncLE, natTransTruncLEOfLE, triangleLEGE, triangleLEGEIsoTriangleLTGE, triangleLEGT, triangleLEGTIsoTriangleLEGE, truncGELE, truncGELEIsoLEGE, truncGELEIsoTruncGELT, truncGEδLE, truncGT, truncGTIsoTruncGE, truncGTδLE, truncGTπ, truncLE, truncLEGE, truncLEIsoTruncLT, truncLEι	19
Theorems descTruncGT_aux, instAdditiveTruncGT, instAdditiveTruncLE, instIsGEObjTruncGELE, instIsGEObjTruncGT, instIsGEObjTruncGTHAddIntOfNat, instIsGEObjTruncGTHSubIntOfNat, instIsGEObjTruncLE, instIsGEObjTruncLE_1, instIsIsoAppTruncLEιOfIsLE, instIsIsoMapTruncLEAppTruncLEι, instIsLEObjTruncGELE, instIsLEObjTruncGT, instIsLEObjTruncLE, instIsLEObjTruncLE_1, isGE_iff_isIso_truncGTπ_app, isGE_iff_isZero_truncLE_obj, isGE_truncGT_obj, isIso_truncGT_map_iff, isIso_truncGT_map_truncGTπ_app, isIso_truncLE_map_iff, isIso_truncLE_map_truncLEι_app, isIso₁_truncLE_map_of_isGE, isIso₂_truncGT_map_of_isLE, isLE_iff_isIso_truncLEι_app, isLE_iff_isZero_truncGT_obj, isLE_truncLE_obj, isZero_truncLE_obj_of_isGE, liftTruncLE_aux, liftTruncLE_ι, liftTruncLE_ι_assoc, natTransTruncLEOfLE_refl, natTransTruncLEOfLE_refl_app, natTransTruncLEOfLE_trans, natTransTruncLEOfLE_trans_app, natTransTruncLEOfLE_trans_app_assoc, natTransTruncLEOfLE_ι, natTransTruncLEOfLE_ι_app, natTransTruncLEOfLE_ι_app_assoc, natTransTruncLEOfLE_ι_assoc, to_truncLE_obj_ext, triangleLEGE_distinguished, triangleLEGE_map_hom₁, triangleLEGE_map_hom₂, triangleLEGE_map_hom₃, triangleLEGE_obj_mor₁, triangleLEGE_obj_mor₂, triangleLEGE_obj_mor₃, triangleLEGE_obj_obj₁, triangleLEGE_obj_obj₂, triangleLEGE_obj_obj₃, triangleLEGT_distinguished, triangleLEGT_map_hom₁, triangleLEGT_map_hom₂, triangleLEGT_map_hom₃, triangleLEGT_obj_mor₁, triangleLEGT_obj_mor₂, triangleLEGT_obj_mor₃, triangleLEGT_obj_obj₁, triangleLEGT_obj_obj₂, triangleLEGT_obj_obj₃, truncLEIsoTruncLT_hom_ι, truncLEIsoTruncLT_hom_ι_app, truncLEIsoTruncLT_hom_ι_app_assoc, truncLEIsoTruncLT_hom_ι_assoc, truncLEIsoTruncLT_inv_ι, truncLEIsoTruncLT_inv_ι_app, truncLEIsoTruncLT_inv_ι_app_assoc, truncLEIsoTruncLT_inv_ι_assoc, π_descTruncGT, π_descTruncGT_assoc, π_truncGTIsoTruncGE_hom, π_truncGTIsoTruncGE_hom_assoc, π_truncGTIsoTruncGE_hom_ι_app, π_truncGTIsoTruncGE_hom_ι_app_assoc, π_truncGTIsoTruncGE_inv, π_truncGTIsoTruncGE_inv_assoc, π_truncGTIsoTruncGE_inv_ι_app, π_truncGTIsoTruncGE_inv_ι_app_assoc	79
Total	98

CategoryTheory.Triangulated.TStructure

Definitions

Name	Category	Theorems
descTruncGT 📖	CompOp	2 math math: π_descTruncGT_assoc, π_descTruncGT
liftTruncLE 📖	CompOp	2 math math: liftTruncLE_ι_assoc, liftTruncLE_ι
natTransTruncLEOfLE 📖	CompOp	9 math math: natTransTruncLEOfLE_ι_assoc, natTransTruncLEOfLE_ι, natTransTruncLEOfLE_trans, natTransTruncLEOfLE_refl, natTransTruncLEOfLE_trans_app, natTransTruncLEOfLE_ι_app, natTransTruncLEOfLE_refl_app, natTransTruncLEOfLE_ι_app_assoc, natTransTruncLEOfLE_trans_app_assoc
triangleLEGE 📖	CompOp	10 math math: triangleLEGE_map_hom₃, triangleLEGE_obj_mor₂, triangleLEGE_distinguished, triangleLEGE_map_hom₁, triangleLEGE_obj_obj₁, triangleLEGE_obj_obj₂, triangleLEGE_obj_mor₃, triangleLEGE_obj_mor₁, triangleLEGE_map_hom₂, triangleLEGE_obj_obj₃
triangleLEGEIsoTriangleLTGE 📖	CompOp	—
triangleLEGT 📖	CompOp	10 math math: triangleLEGT_map_hom₁, triangleLEGT_obj_obj₃, triangleLEGT_obj_obj₁, triangleLEGT_obj_obj₂, triangleLEGT_obj_mor₃, triangleLEGT_obj_mor₁, triangleLEGT_distinguished, triangleLEGT_map_hom₃, triangleLEGT_obj_mor₂, triangleLEGT_map_hom₂
triangleLEGTIsoTriangleLEGE 📖	CompOp	—
truncGELE 📖	CompOp	2 math math: instIsLEObjTruncGELE, instIsGEObjTruncGELE
truncGELEIsoLEGE 📖	CompOp	—
truncGELEIsoTruncGELT 📖	CompOp	—
truncGEδLE 📖	CompOp	4 math math: triangleLEGE_map_hom₃, triangleLEGE_map_hom₁, triangleLEGE_obj_mor₃, triangleLEGE_map_hom₂
truncGT 📖	CompOp	28 math math: instIsLEObjTruncGT, π_descTruncGT_assoc, π_truncGTIsoTruncGE_hom_ι_app_assoc, isGE_iff_isIso_truncGTπ_app, π_truncGTIsoTruncGE_inv_ι_app, triangleLEGT_map_hom₁, triangleLEGT_obj_obj₃, instAdditiveTruncGT, triangleLEGT_obj_mor₃, isLE_iff_isZero_truncGT_obj, isIso_truncGT_map_truncGTπ_app, π_truncGTIsoTruncGE_inv_ι_app_assoc, π_truncGTIsoTruncGE_inv_assoc, π_truncGTIsoTruncGE_hom, instIsGEObjTruncGTHSubIntOfNat, isIso₂_truncGT_map_of_isLE, isIso_truncGT_map_iff, π_truncGTIsoTruncGE_hom_assoc, π_truncGTIsoTruncGE_inv, instIsGEObjTruncGT, π_descTruncGT, descTruncGT_aux, π_truncGTIsoTruncGE_hom_ι_app, triangleLEGT_map_hom₃, isGE_truncGT_obj, triangleLEGT_obj_mor₂, triangleLEGT_map_hom₂, instIsGEObjTruncGTHAddIntOfNat
truncGTIsoTruncGE 📖	CompOp	8 math math: π_truncGTIsoTruncGE_hom_ι_app_assoc, π_truncGTIsoTruncGE_inv_ι_app, π_truncGTIsoTruncGE_inv_ι_app_assoc, π_truncGTIsoTruncGE_inv_assoc, π_truncGTIsoTruncGE_hom, π_truncGTIsoTruncGE_hom_assoc, π_truncGTIsoTruncGE_inv, π_truncGTIsoTruncGE_hom_ι_app
truncGTδLE 📖	CompOp	4 math math: triangleLEGT_map_hom₁, triangleLEGT_obj_mor₃, triangleLEGT_map_hom₃, triangleLEGT_map_hom₂
truncGTπ 📖	CompOp	18 math math: π_descTruncGT_assoc, π_truncGTIsoTruncGE_hom_ι_app_assoc, isGE_iff_isIso_truncGTπ_app, π_truncGTIsoTruncGE_inv_ι_app, triangleLEGT_map_hom₁, isIso_truncGT_map_truncGTπ_app, π_truncGTIsoTruncGE_inv_ι_app_assoc, π_truncGTIsoTruncGE_inv_assoc, π_truncGTIsoTruncGE_hom, isIso_truncGT_map_iff, π_truncGTIsoTruncGE_hom_assoc, π_truncGTIsoTruncGE_inv, π_descTruncGT, descTruncGT_aux, π_truncGTIsoTruncGE_hom_ι_app, triangleLEGT_map_hom₃, triangleLEGT_obj_mor₂, triangleLEGT_map_hom₂
truncLE 📖	CompOp	46 math math: instAdditiveTruncLE, natTransTruncLEOfLE_ι_assoc, triangleLEGE_map_hom₃, isIso_truncLE_map_truncLEι_app, truncLEIsoTruncLT_hom_ι_assoc, isLE_iff_isIso_truncLEι_app, instIsLEObjTruncLE_1, triangleLEGT_map_hom₁, instIsGEObjTruncLE_1, truncLEIsoTruncLT_hom_ι, instIsIsoAppTruncLEιOfIsLE, triangleLEGT_obj_obj₁, instIsIsoMapTruncLEAppTruncLEι, truncLEIsoTruncLT_inv_ι_app, natTransTruncLEOfLE_ι, liftTruncLE_ι_assoc, triangleLEGT_obj_mor₃, natTransTruncLEOfLE_trans, natTransTruncLEOfLE_refl, natTransTruncLEOfLE_trans_app, natTransTruncLEOfLE_ι_app, natTransTruncLEOfLE_refl_app, natTransTruncLEOfLE_ι_app_assoc, instIsGEObjTruncLE, isGE_iff_isZero_truncLE_obj, truncLEIsoTruncLT_inv_ι_assoc, natTransTruncLEOfLE_trans_app_assoc, instIsLEObjTruncLE, triangleLEGE_map_hom₁, isIso₁_truncLE_map_of_isGE, triangleLEGT_obj_mor₁, truncLEIsoTruncLT_inv_ι, truncLEIsoTruncLT_hom_ι_app_assoc, triangleLEGE_obj_obj₁, isIso_truncLE_map_iff, liftTruncLE_aux, triangleLEGT_map_hom₃, isZero_truncLE_obj_of_isGE, isLE_truncLE_obj, truncLEIsoTruncLT_hom_ι_app, triangleLEGT_map_hom₂, triangleLEGE_obj_mor₃, triangleLEGE_obj_mor₁, triangleLEGE_map_hom₂, truncLEIsoTruncLT_inv_ι_app_assoc, liftTruncLE_ι
truncLEGE 📖	CompOp	—
truncLEIsoTruncLT 📖	CompOp	8 math math: truncLEIsoTruncLT_hom_ι_assoc, truncLEIsoTruncLT_hom_ι, truncLEIsoTruncLT_inv_ι_app, truncLEIsoTruncLT_inv_ι_assoc, truncLEIsoTruncLT_inv_ι, truncLEIsoTruncLT_hom_ι_app_assoc, truncLEIsoTruncLT_hom_ι_app, truncLEIsoTruncLT_inv_ι_app_assoc
truncLEι 📖	CompOp	28 math math: natTransTruncLEOfLE_ι_assoc, triangleLEGE_map_hom₃, isIso_truncLE_map_truncLEι_app, truncLEIsoTruncLT_hom_ι_assoc, isLE_iff_isIso_truncLEι_app, triangleLEGT_map_hom₁, truncLEIsoTruncLT_hom_ι, instIsIsoAppTruncLEιOfIsLE, instIsIsoMapTruncLEAppTruncLEι, truncLEIsoTruncLT_inv_ι_app, natTransTruncLEOfLE_ι, liftTruncLE_ι_assoc, natTransTruncLEOfLE_ι_app, natTransTruncLEOfLE_ι_app_assoc, truncLEIsoTruncLT_inv_ι_assoc, triangleLEGE_map_hom₁, triangleLEGT_obj_mor₁, truncLEIsoTruncLT_inv_ι, truncLEIsoTruncLT_hom_ι_app_assoc, isIso_truncLE_map_iff, liftTruncLE_aux, triangleLEGT_map_hom₃, truncLEIsoTruncLT_hom_ι_app, triangleLEGT_map_hom₂, triangleLEGE_obj_mor₁, triangleLEGE_map_hom₂, truncLEIsoTruncLT_inv_ι_app_assoc, liftTruncLE_ι

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
descTruncGT_aux 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncGT CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.id CategoryTheory.NatTrans.app truncGTπ	—	CategoryTheory.Pretriangulated.Triangle.yoneda_exact₂ triangleLEGT_distinguished zero_of_isLE_of_isGE instIsLEObjTruncLE
instAdditiveTruncGT 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.Additive truncGT	—	instAdditiveTruncGE
instAdditiveTruncLE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.Additive truncLE	—	instAdditiveTruncLT
instIsGEObjTruncGELE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE CategoryTheory.Functor.obj truncGELE	—	instIsGEObjTruncGE
instIsGEObjTruncGT 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE CategoryTheory.Functor.obj truncGT	—	instIsGEObjTruncGE_1
instIsGEObjTruncGTHAddIntOfNat 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE CategoryTheory.Functor.obj truncGT	—	isGE_truncGT_obj
instIsGEObjTruncGTHSubIntOfNat 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE CategoryTheory.Functor.obj truncGT	—	isGE_truncGT_obj
instIsGEObjTruncLE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE CategoryTheory.Functor.obj truncLE	—	instIsGEObjTruncLT
instIsGEObjTruncLE_1 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE CategoryTheory.Functor.obj truncLE	—	instIsGEObjTruncLT
instIsIsoAppTruncLEιOfIsLE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.IsIso CategoryTheory.Functor.obj truncLE CategoryTheory.Functor.id CategoryTheory.NatTrans.app truncLEι	—	isLE_iff_isIso_truncLEι_app
instIsIsoMapTruncLEAppTruncLEι 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.IsIso CategoryTheory.Functor.obj truncLE CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app truncLEι	—	isIso_truncLE_map_truncLEι_app
instIsLEObjTruncGELE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE CategoryTheory.Functor.obj truncGELE	—	instIsLEObjTruncGE instIsLEObjTruncLE
instIsLEObjTruncGT 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE CategoryTheory.Functor.obj truncGT	—	instIsLEObjTruncGE
instIsLEObjTruncLE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE CategoryTheory.Functor.obj truncLE	—	isLE_truncLE_obj
instIsLEObjTruncLE_1 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE CategoryTheory.Functor.obj truncLE	—	instIsLEObjTruncLT
isGE_iff_isIso_truncGTπ_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.id truncGT CategoryTheory.NatTrans.app truncGTπ	—	isGE_iff_isIso_truncGEπ_app CategoryTheory.MorphismProperty.arrow_mk_iso_iff CategoryTheory.MorphismProperty.RespectsIso.isomorphisms CategoryTheory.Category.id_comp π_truncGTIsoTruncGE_inv_ι_app
isGE_iff_isZero_truncLE_obj 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj truncLE	—	isGE_iff_isIso_truncGEπ_app CategoryTheory.Pretriangulated.Triangle.isZero₁_iff_isIso₂ triangleLEGE_distinguished
isGE_truncGT_obj 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE CategoryTheory.Functor.obj truncGT	—	isGE_truncGE_obj
isIso_truncGT_map_iff 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.IsIso CategoryTheory.Functor.obj truncGT CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.app CategoryTheory.Functor.id truncGTπ IsLE	—	isIso_truncGE_map_iff
isIso_truncGT_map_truncGTπ_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.IsIso CategoryTheory.Functor.obj truncGT CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app truncGTπ	—	isIso_truncGE_map_truncGEπ_app
isIso_truncLE_map_iff 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.IsIso CategoryTheory.Functor.obj truncLE CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.id CategoryTheory.NatTrans.app truncLEι IsGE	—	isIso_truncLT_map_iff
isIso_truncLE_map_truncLEι_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.IsIso CategoryTheory.Functor.obj truncLE CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app truncLEι	—	isIso_truncLT_map_truncLTι_app
isIso₁_truncLE_map_of_isGE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.IsIso CategoryTheory.Functor.obj truncLE CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle.mor₁	—	isIso₁_truncLT_map_of_isGE
isIso₂_truncGT_map_of_isLE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.IsIso CategoryTheory.Functor.obj truncGT CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle.mor₂	—	isIso₂_truncGE_map_of_isLE
isLE_iff_isIso_truncLEι_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE CategoryTheory.IsIso CategoryTheory.Functor.obj truncLE CategoryTheory.Functor.id CategoryTheory.NatTrans.app truncLEι	—	isLE_iff_isIso_truncLTι_app
isLE_iff_isZero_truncGT_obj 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj truncGT	—	isLE_iff_isIso_truncLEι_app CategoryTheory.Pretriangulated.Triangle.isZero₃_iff_isIso₁ triangleLEGT_distinguished
isLE_truncLE_obj 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE CategoryTheory.Functor.obj truncLE	—	isLE_truncLT_obj
isZero_truncLE_obj_of_isGE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj truncLE	—	isGE_iff_isZero_truncLE_obj
liftTruncLE_aux 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncLE CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.id CategoryTheory.NatTrans.app truncLEι	—	CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂ triangleLEGT_distinguished zero_of_isLE_of_isGE instIsGEObjTruncGTHAddIntOfNat
liftTruncLE_ι 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncLE CategoryTheory.Functor.id liftTruncLE CategoryTheory.NatTrans.app truncLEι	—	liftTruncLE_aux
liftTruncLE_ι_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncLE liftTruncLE CategoryTheory.NatTrans.app CategoryTheory.Functor.id truncLEι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' liftTruncLE_ι
natTransTruncLEOfLE_refl 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	natTransTruncLEOfLE CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category truncLE	—	natTransTruncLTOfLE_refl
natTransTruncLEOfLE_refl_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.NatTrans.app truncLE natTransTruncLEOfLE CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	CategoryTheory.congr_app natTransTruncLEOfLE_refl
natTransTruncLEOfLE_trans 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category truncLE natTransTruncLEOfLE LE.le.trans PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	—	natTransTruncLTOfLE_trans
natTransTruncLEOfLE_trans_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncLE CategoryTheory.NatTrans.app natTransTruncLEOfLE LE.le.trans PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	—	CategoryTheory.congr_app LE.le.trans natTransTruncLEOfLE_trans
natTransTruncLEOfLE_trans_app_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncLE CategoryTheory.NatTrans.app natTransTruncLEOfLE LE.le.trans PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	—	LE.le.trans CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' natTransTruncLEOfLE_trans_app
natTransTruncLEOfLE_ι 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category truncLE CategoryTheory.Functor.id natTransTruncLEOfLE truncLEι	—	CategoryTheory.NatTrans.ext' natTransTruncLEOfLE_ι_app
natTransTruncLEOfLE_ι_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncLE CategoryTheory.Functor.id CategoryTheory.NatTrans.app natTransTruncLEOfLE truncLEι	—	natTransTruncLTOfLE_ι_app
natTransTruncLEOfLE_ι_app_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncLE CategoryTheory.NatTrans.app natTransTruncLEOfLE CategoryTheory.Functor.id truncLEι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' natTransTruncLEOfLE_ι_app
natTransTruncLEOfLE_ι_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category truncLE natTransTruncLEOfLE CategoryTheory.Functor.id truncLEι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' natTransTruncLEOfLE_ι
to_truncLE_obj_ext 📖	—	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncLE CategoryTheory.Functor.id CategoryTheory.NatTrans.app truncLEι	—	—	add_sub_cancel_right CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.Functor.instIsSplitMonoApp CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom to_truncLT_obj_ext CategoryTheory.Category.assoc truncLEIsoTruncLT_hom_ι_app
triangleLEGE_distinguished 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.triangleCategory triangleLEGE	—	CategoryTheory.Pretriangulated.isomorphic_distinguished triangleLTGE_distinguished
triangleLEGE_map_hom₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ CategoryTheory.Functor.obj truncLE CategoryTheory.Functor.id truncGE CategoryTheory.NatTrans.app truncLEι truncGEπ CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid truncGEδLE CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLEGE	—	—
triangleLEGE_map_hom₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ CategoryTheory.Functor.obj truncLE CategoryTheory.Functor.id truncGE CategoryTheory.NatTrans.app truncLEι truncGEπ CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid truncGEδLE CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLEGE	—	—
triangleLEGE_map_hom₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ CategoryTheory.Functor.obj truncLE CategoryTheory.Functor.id truncGE CategoryTheory.NatTrans.app truncLEι truncGEπ CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid truncGEδLE CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLEGE	—	—
triangleLEGE_obj_mor₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.mor₁ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLEGE CategoryTheory.NatTrans.app truncLE CategoryTheory.Functor.id truncLEι	—	—
triangleLEGE_obj_mor₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.mor₂ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLEGE CategoryTheory.NatTrans.app CategoryTheory.Functor.id truncGE truncGEπ	—	—
triangleLEGE_obj_mor₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLEGE CategoryTheory.NatTrans.app truncGE CategoryTheory.Functor.comp truncLE CategoryTheory.shiftFunctor Int.instAddMonoid truncGEδLE	—	—
triangleLEGE_obj_obj₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLEGE truncLE	—	—
triangleLEGE_obj_obj₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLEGE	—	—
triangleLEGE_obj_obj₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLEGE truncGE	—	—
triangleLEGT_distinguished 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.triangleCategory triangleLEGT	—	CategoryTheory.Pretriangulated.isomorphic_distinguished triangleLEGE_distinguished
triangleLEGT_map_hom₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ CategoryTheory.Functor.obj truncLE CategoryTheory.Functor.id truncGT CategoryTheory.NatTrans.app truncLEι truncGTπ CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid truncGTδLE CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLEGT	—	—
triangleLEGT_map_hom₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ CategoryTheory.Functor.obj truncLE CategoryTheory.Functor.id truncGT CategoryTheory.NatTrans.app truncLEι truncGTπ CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid truncGTδLE CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLEGT	—	—
triangleLEGT_map_hom₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ CategoryTheory.Functor.obj truncLE CategoryTheory.Functor.id truncGT CategoryTheory.NatTrans.app truncLEι truncGTπ CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid truncGTδLE CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLEGT	—	—
triangleLEGT_obj_mor₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.mor₁ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLEGT CategoryTheory.NatTrans.app truncLE CategoryTheory.Functor.id truncLEι	—	—
triangleLEGT_obj_mor₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.mor₂ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLEGT CategoryTheory.NatTrans.app CategoryTheory.Functor.id truncGT truncGTπ	—	—
triangleLEGT_obj_mor₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLEGT CategoryTheory.NatTrans.app truncGT CategoryTheory.Functor.comp truncLE CategoryTheory.shiftFunctor Int.instAddMonoid truncGTδLE	—	—
triangleLEGT_obj_obj₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLEGT truncLE	—	—
triangleLEGT_obj_obj₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLEGT	—	—
triangleLEGT_obj_obj₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLEGT truncGT	—	—
truncLEIsoTruncLT_hom_ι 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category truncLE truncLT CategoryTheory.Functor.id CategoryTheory.Iso.hom truncLEIsoTruncLT truncLTι truncLEι	—	CategoryTheory.Category.id_comp
truncLEIsoTruncLT_hom_ι_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncLE truncLT CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category truncLEIsoTruncLT truncLTι truncLEι	—	CategoryTheory.congr_app truncLEIsoTruncLT_hom_ι
truncLEIsoTruncLT_hom_ι_app_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncLE truncLT CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category truncLEIsoTruncLT CategoryTheory.Functor.id truncLTι truncLEι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' truncLEIsoTruncLT_hom_ι_app
truncLEIsoTruncLT_hom_ι_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category truncLE truncLT CategoryTheory.Iso.hom truncLEIsoTruncLT CategoryTheory.Functor.id truncLTι truncLEι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' truncLEIsoTruncLT_hom_ι
truncLEIsoTruncLT_inv_ι 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category truncLT truncLE CategoryTheory.Functor.id CategoryTheory.Iso.inv truncLEIsoTruncLT truncLEι truncLTι	—	CategoryTheory.Category.id_comp
truncLEIsoTruncLT_inv_ι_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncLT truncLE CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category truncLEIsoTruncLT truncLEι truncLTι	—	CategoryTheory.congr_app truncLEIsoTruncLT_inv_ι
truncLEIsoTruncLT_inv_ι_app_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncLT truncLE CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category truncLEIsoTruncLT CategoryTheory.Functor.id truncLEι truncLTι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' truncLEIsoTruncLT_inv_ι_app
truncLEIsoTruncLT_inv_ι_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category truncLT truncLE CategoryTheory.Iso.inv truncLEIsoTruncLT CategoryTheory.Functor.id truncLEι truncLTι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' truncLEIsoTruncLT_inv_ι
π_descTruncGT 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id truncGT CategoryTheory.NatTrans.app truncGTπ descTruncGT	—	descTruncGT_aux
π_descTruncGT_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncGT CategoryTheory.NatTrans.app CategoryTheory.Functor.id truncGTπ descTruncGT	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_descTruncGT
π_truncGTIsoTruncGE_hom 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id truncGT truncGE truncGTπ CategoryTheory.Iso.hom truncGTIsoTruncGE truncGEπ	—	CategoryTheory.Category.comp_id
π_truncGTIsoTruncGE_hom_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id truncGT truncGTπ truncGE CategoryTheory.Iso.hom truncGTIsoTruncGE truncGEπ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_truncGTIsoTruncGE_hom
π_truncGTIsoTruncGE_hom_ι_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id truncGT truncGE CategoryTheory.NatTrans.app truncGTπ CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category truncGTIsoTruncGE truncGEπ	—	CategoryTheory.congr_app π_truncGTIsoTruncGE_hom
π_truncGTIsoTruncGE_hom_ι_app_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncGT CategoryTheory.NatTrans.app CategoryTheory.Functor.id truncGTπ truncGE CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category truncGTIsoTruncGE truncGEπ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_truncGTIsoTruncGE_hom_ι_app
π_truncGTIsoTruncGE_inv 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id truncGE truncGT truncGEπ CategoryTheory.Iso.inv truncGTIsoTruncGE truncGTπ	—	CategoryTheory.Category.comp_id
π_truncGTIsoTruncGE_inv_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id truncGE truncGEπ truncGT CategoryTheory.Iso.inv truncGTIsoTruncGE truncGTπ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_truncGTIsoTruncGE_inv
π_truncGTIsoTruncGE_inv_ι_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id truncGE truncGT CategoryTheory.NatTrans.app truncGEπ CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category truncGTIsoTruncGE truncGTπ	—	CategoryTheory.congr_app π_truncGTIsoTruncGE_inv
π_truncGTIsoTruncGE_inv_ι_app_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncGE CategoryTheory.NatTrans.app CategoryTheory.Functor.id truncGEπ truncGT CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category truncGTIsoTruncGE truncGTπ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_truncGTIsoTruncGE_inv_ι_app

---

← Back to Index