TruncLTGE

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

Statistics

Metric	Count
Definitions descTruncGE, liftTruncLT, natTransTriangleLTGEOfLE, natTransTruncGEOfLE, natTransTruncLTOfLE, triangleLTGE, triangleLTLTGELT, truncGE, truncGELT, truncGELTIsoLTGE, truncGELTToLTGE, truncGELTδLT, truncGEδLT, truncGEπ, truncLT, truncLTGE, truncLTι	17
Theorems descTruncGE_aux, from_truncGE_obj_ext, instAdditiveTruncGE, instAdditiveTruncLT, instIsGEObjTruncGE, instIsGEObjTruncGELT, instIsGEObjTruncGE_1, instIsGEObjTruncLT, instIsGEObjTruncLTGE, instIsGEObj₃ObjTriangleTriangleLTGE, instIsGEOfNat, instIsIsoAppTruncGEπOfIsGE, instIsIsoAppTruncLTιObjTruncGETruncLT, instIsIsoFunctorTruncGELTToLTGE, instIsIsoMapTruncGEAppTruncGEπ, instIsIsoMapTruncLTAppTruncLTι, instIsIsoMapTruncLTTruncGEAppTruncLTι, instIsLEObjTruncGE, instIsLEObjTruncGELTHSubIntOfNat, instIsLEObjTruncLT, instIsLEObjTruncLTGEHSubIntOfNat, instIsLEObjTruncLTHAddIntOfNat, instIsLEObjTruncLTHSubIntOfNat, instIsLEObj₁ObjTriangleTriangleLTGEHSubIntOfNat, instIsLEOfNat, instIsTriangulatedBounded, instIsTriangulatedMinus, instIsTriangulatedPlus, isGE_iff_isIso_truncGEπ_app, isGE_iff_isZero_truncLT_obj, isGE_iff_orthogonal, isGE_of_isZero, isGE_truncGE_obj, isGE₂, isIso_truncGE_map_iff, isIso_truncGE_map_truncGEπ_app, isIso_truncLT_map_iff, isIso_truncLT_map_truncLTι_app, isIso₁_truncLT_map_of_isGE, isIso₂_truncGE_map_of_isLE, isLE_iff_isIso_truncLTι_app, isLE_iff_isZero_truncGE_obj, isLE_iff_orthogonal, isLE_of_isZero, isLE_truncLT_obj, isLE₂, isZero_truncGE_obj_of_isLE, isZero_truncLT_obj_of_isGE, liftTruncLT_aux, liftTruncLT_ι, liftTruncLT_ι_assoc, natTransTriangleLTGEOfLE_refl, natTransTriangleLTGEOfLE_trans, natTransTruncGEOfLE_refl, natTransTruncGEOfLE_refl_app, natTransTruncGEOfLE_trans, natTransTruncGEOfLE_trans_app, natTransTruncLTOfLE_refl, natTransTruncLTOfLE_refl_app, natTransTruncLTOfLE_trans, natTransTruncLTOfLE_trans_app, natTransTruncLTOfLE_ι, natTransTruncLTOfLE_ι_app, natTransTruncLTOfLE_ι_app_assoc, natTransTruncLTOfLE_ι_assoc, to_truncLT_obj_ext, triangleLTGE_distinguished, triangleLTGE_map_hom₁, triangleLTGE_map_hom₂, triangleLTGE_map_hom₃, triangleLTGE_obj_mor₁, triangleLTGE_obj_mor₂, triangleLTGE_obj_mor₃, triangleLTGE_obj_obj₁, triangleLTGE_obj_obj₂, triangleLTGE_obj_obj₃, triangleLTLTGELT_distinguished, triangleLTLTGELT_map_hom₁, triangleLTLTGELT_map_hom₂, triangleLTLTGELT_map_hom₃, triangleLTLTGELT_obj_mor₁, triangleLTLTGELT_obj_mor₂, triangleLTLTGELT_obj_mor₃, triangleLTLTGELT_obj_obj₁, triangleLTLTGELT_obj_obj₂, triangleLTLTGELT_obj_obj₃, triangle_iso_exists, triangle_map_exists, triangle_map_ext, truncGELTToLTGE_app_pentagon, truncGELTToLTGE_app_pentagon_assoc, truncGELTToLTGE_app_pentagon_uniqueness, truncGELTδLT_app, truncGE_map_truncGEπ_app, truncGE_map_truncGEπ_app_assoc, truncGEδLT_comp_natTransTruncLTOfLE_app, truncGEδLT_comp_natTransTruncLTOfLE_app_assoc, truncGEδLT_comp_truncLTι, truncGEδLT_comp_truncLTι_app, truncGEδLT_comp_truncLTι_app_assoc, truncGEδLT_comp_truncLTι_assoc, truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE, truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE_assoc, truncGEπ_comp_truncGEδLT, truncGEπ_comp_truncGEδLT_app, truncGEπ_comp_truncGEδLT_app_assoc, truncGEπ_comp_truncGEδLT_assoc, truncGEπ_naturality, truncGEπ_naturality_assoc, truncLT_map_truncGE_map_truncLTι_app_fac, truncLT_map_truncGE_map_truncLTι_app_fac_assoc, truncLT_map_truncLTι_app, truncLT_map_truncLTι_app_assoc, truncLTι_comp_truncGEπ, truncLTι_comp_truncGEπ_app, truncLTι_comp_truncGEπ_app_assoc, truncLTι_comp_truncGEπ_assoc, π_descTruncGE, π_descTruncGE_assoc, π_natTransTruncGEOfLE, π_natTransTruncGEOfLE_app, π_natTransTruncGEOfLE_app_assoc, π_natTransTruncGEOfLE_assoc	123
Total	140

CategoryTheory.Triangulated.TStructure

Definitions

Name	Category	Theorems
descTruncGE 📖	CompOp	2 math math: π_descTruncGE, π_descTruncGE_assoc
liftTruncLT 📖	CompOp	2 math math: liftTruncLT_ι_assoc, liftTruncLT_ι
natTransTriangleLTGEOfLE 📖	CompOp	2 math math: natTransTriangleLTGEOfLE_refl, natTransTriangleLTGEOfLE_trans
natTransTruncGEOfLE 📖	CompOp	12 math math: natTransTruncGEOfLE_trans_app, π_natTransTruncGEOfLE_app, π_natTransTruncGEOfLE_app_assoc, natTransTruncGEOfLE_refl, π_natTransTruncGEOfLE_assoc, natTransTruncGEOfLE_trans, truncGEδLT_comp_natTransTruncLTOfLE_app, π_natTransTruncGEOfLE, truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE_assoc, truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE, natTransTruncGEOfLE_refl_app, truncGEδLT_comp_natTransTruncLTOfLE_app_assoc
natTransTruncLTOfLE 📖	CompOp	16 math math: natTransTruncLTOfLE_trans, triangleLTLTGELT_map_hom₁, natTransTruncLTOfLE_refl, natTransTruncLTOfLE_ι_app_assoc, natTransTruncLTOfLE_trans_app, triangleLTLTGELT_map_hom₂, truncGEδLT_comp_natTransTruncLTOfLE_app, triangleLTLTGELT_map_hom₃, truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE_assoc, truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE, natTransTruncLTOfLE_ι, natTransTruncLTOfLE_ι_app, truncGEδLT_comp_natTransTruncLTOfLE_app_assoc, natTransTruncLTOfLE_refl_app, triangleLTLTGELT_obj_mor₁, natTransTruncLTOfLE_ι_assoc
triangleLTGE 📖	CompOp	14 math math: triangleLTGE_obj_mor₁, triangleLTGE_obj_obj₃, instIsGEObj₃ObjTriangleTriangleLTGE, triangleLTGE_map_hom₃, triangleLTGE_map_hom₂, triangleLTGE_obj_mor₃, triangleLTGE_obj_obj₁, instIsLEObj₁ObjTriangleTriangleLTGEHSubIntOfNat, triangleLTGE_distinguished, triangleLTGE_obj_mor₂, natTransTriangleLTGEOfLE_refl, triangleLTGE_map_hom₁, triangleLTGE_obj_obj₂, natTransTriangleLTGEOfLE_trans
triangleLTLTGELT 📖	CompOp	10 math math: triangleLTLTGELT_distinguished, triangleLTLTGELT_obj_mor₂, triangleLTLTGELT_obj_obj₁, triangleLTLTGELT_map_hom₁, triangleLTLTGELT_obj_obj₃, triangleLTLTGELT_obj_mor₃, triangleLTLTGELT_map_hom₂, triangleLTLTGELT_map_hom₃, triangleLTLTGELT_obj_obj₂, triangleLTLTGELT_obj_mor₁
truncGE 📖	CompOp	78 math math: truncGEδLT_comp_truncLTι, truncGEπ_comp_truncGEδLT_assoc, instIsIsoMapTruncLTTruncGEAppTruncLTι, truncLT_map_truncGE_map_truncLTι_app_fac_assoc, isLE_iff_isZero_truncGE_obj, triangleLEGE_map_hom₃, triangleLEGE_obj_mor₂, truncGEπ_naturality_assoc, natTransTruncGEOfLE_trans_app, triangleLTLTGELT_obj_mor₂, isZero_truncGE_obj_of_isLE, isGE_truncGE_obj, instIsGEObjTruncGE_1, π_truncGTIsoTruncGE_hom_ι_app_assoc, truncGELTToLTGE_app_pentagon_assoc, truncGEπ_comp_truncGEδLT_app_assoc, π_truncGTIsoTruncGE_inv_ι_app, triangleLTGE_obj_obj₃, truncGEδLT_comp_truncLTι_app, truncLTι_comp_truncGEπ_assoc, π_natTransTruncGEOfLE_app, triangleLTLTGELT_map_hom₁, π_natTransTruncGEOfLE_app_assoc, triangleLTLTGELT_obj_obj₃, triangleLTLTGELT_obj_mor₃, π_descTruncGE, natTransTruncGEOfLE_refl, triangleLTGE_map_hom₃, π_truncGTIsoTruncGE_inv_ι_app_assoc, truncGE_map_truncGEπ_app_assoc, π_natTransTruncGEOfLE_assoc, π_truncGTIsoTruncGE_inv_assoc, π_truncGTIsoTruncGE_hom, instIsLEObjTruncGE, natTransTruncGEOfLE_trans, triangleLTLTGELT_map_hom₂, triangleLTGE_map_hom₂, triangleLTGE_obj_mor₃, isGE_iff_isIso_truncGEπ_app, isIso₂_truncGE_map_of_isLE, truncGEδLT_comp_natTransTruncLTOfLE_app, π_natTransTruncGEOfLE, isIso_truncGE_map_truncGEπ_app, triangleLEGE_map_hom₁, triangleLTLTGELT_map_hom₃, truncLTι_comp_truncGEπ_app_assoc, π_truncGTIsoTruncGE_hom_assoc, truncGEδLT_comp_truncLTι_assoc, instIsGEObjTruncGE, instIsIsoMapTruncGEAppTruncGEπ, π_truncGTIsoTruncGE_inv, truncGEπ_comp_truncGEδLT, instAdditiveTruncGE, truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE_assoc, truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE, triangleLTGE_obj_mor₂, π_truncGTIsoTruncGE_hom_ι_app, triangleLTGE_map_hom₁, truncGEπ_naturality, descTruncGE_aux, eTruncGE_obj_coe, truncLTι_comp_truncGEπ, truncGEδLT_comp_truncLTι_app_assoc, truncGELTδLT_app, natTransTruncGEOfLE_refl_app, truncGEπ_comp_truncGEδLT_app, triangleLEGE_obj_mor₃, truncGELTToLTGE_app_pentagon, instIsIsoAppTruncLTιObjTruncGETruncLT, truncGEδLT_comp_natTransTruncLTOfLE_app_assoc, truncLTι_comp_truncGEπ_app, triangleLEGE_map_hom₂, instIsIsoAppTruncGEπOfIsGE, triangleLEGE_obj_obj₃, π_descTruncGE_assoc, truncLT_map_truncGE_map_truncLTι_app_fac, isIso_truncGE_map_iff, truncGE_map_truncGEπ_app
truncGELT 📖	CompOp	9 math math: truncLT_map_truncGE_map_truncLTι_app_fac_assoc, truncGELTToLTGE_app_pentagon_assoc, instIsLEObjTruncGELTHSubIntOfNat, instIsIsoFunctorTruncGELTToLTGE, truncGELTToLTGE_app_pentagon_uniqueness, truncGELTδLT_app, truncGELTToLTGE_app_pentagon, instIsGEObjTruncGELT, truncLT_map_truncGE_map_truncLTι_app_fac
truncGELTIsoLTGE 📖	CompOp	—
truncGELTToLTGE 📖	CompOp	6 math math: truncLT_map_truncGE_map_truncLTι_app_fac_assoc, truncGELTToLTGE_app_pentagon_assoc, instIsIsoFunctorTruncGELTToLTGE, truncGELTToLTGE_app_pentagon_uniqueness, truncGELTToLTGE_app_pentagon, truncLT_map_truncGE_map_truncLTι_app_fac
truncGELTδLT 📖	CompOp	4 math math: triangleLTLTGELT_map_hom₁, triangleLTLTGELT_map_hom₂, triangleLTLTGELT_map_hom₃, truncGELTδLT_app
truncGEδLT 📖	CompOp	19 math math: truncGEδLT_comp_truncLTι, truncGEπ_comp_truncGEδLT_assoc, truncGEπ_comp_truncGEδLT_app_assoc, truncGEδLT_comp_truncLTι_app, triangleLTLTGELT_obj_mor₃, triangleLTGE_map_hom₃, triangleLTGE_map_hom₂, triangleLTGE_obj_mor₃, truncGEδLT_comp_natTransTruncLTOfLE_app, truncGEδLT_comp_truncLTι_assoc, truncGEπ_comp_truncGEδLT, truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE_assoc, truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE, triangleLTGE_map_hom₁, truncGEδLT_comp_truncLTι_app_assoc, truncGELTδLT_app, eTruncGEδLT_coe, truncGEπ_comp_truncGEδLT_app, truncGEδLT_comp_natTransTruncLTOfLE_app_assoc
truncGEπ 📖	CompOp	47 math math: truncGEπ_comp_truncGEδLT_assoc, triangleLEGE_map_hom₃, triangleLEGE_obj_mor₂, truncGEπ_naturality_assoc, triangleLTLTGELT_obj_mor₂, π_truncGTIsoTruncGE_hom_ι_app_assoc, truncGELTToLTGE_app_pentagon_assoc, truncGEπ_comp_truncGEδLT_app_assoc, π_truncGTIsoTruncGE_inv_ι_app, truncLTι_comp_truncGEπ_assoc, π_natTransTruncGEOfLE_app, triangleLTLTGELT_map_hom₁, π_natTransTruncGEOfLE_app_assoc, π_descTruncGE, triangleLTGE_map_hom₃, π_truncGTIsoTruncGE_inv_ι_app_assoc, truncGE_map_truncGEπ_app_assoc, π_natTransTruncGEOfLE_assoc, π_truncGTIsoTruncGE_inv_assoc, π_truncGTIsoTruncGE_hom, triangleLTLTGELT_map_hom₂, triangleLTGE_map_hom₂, isGE_iff_isIso_truncGEπ_app, π_natTransTruncGEOfLE, isIso_truncGE_map_truncGEπ_app, triangleLEGE_map_hom₁, triangleLTLTGELT_map_hom₃, truncLTι_comp_truncGEπ_app_assoc, π_truncGTIsoTruncGE_hom_assoc, instIsIsoMapTruncGEAppTruncGEπ, π_truncGTIsoTruncGE_inv, truncGEπ_comp_truncGEδLT, triangleLTGE_obj_mor₂, π_truncGTIsoTruncGE_hom_ι_app, triangleLTGE_map_hom₁, truncGEπ_naturality, descTruncGE_aux, truncLTι_comp_truncGEπ, eTruncGEπ_coe, truncGEπ_comp_truncGEδLT_app, truncGELTToLTGE_app_pentagon, truncLTι_comp_truncGEπ_app, triangleLEGE_map_hom₂, instIsIsoAppTruncGEπOfIsGE, π_descTruncGE_assoc, isIso_truncGE_map_iff, truncGE_map_truncGEπ_app
truncLT 📖	CompOp	73 math math: truncGEδLT_comp_truncLTι, truncGEπ_comp_truncGEδLT_assoc, instIsIsoMapTruncLTTruncGEAppTruncLTι, truncLT_map_truncGE_map_truncLTι_app_fac_assoc, instIsIsoMapTruncLTAppTruncLTι, natTransTruncLTOfLE_trans, instIsLEObjTruncLTHSubIntOfNat, truncLEIsoTruncLT_hom_ι_assoc, triangleLTLTGELT_obj_mor₂, truncLT_map_truncLTι_app, triangleLTGE_obj_mor₁, truncGELTToLTGE_app_pentagon_assoc, truncGEπ_comp_truncGEδLT_app_assoc, triangleLTLTGELT_obj_obj₁, truncGEδLT_comp_truncLTι_app, truncLTι_comp_truncGEπ_assoc, isIso_truncLT_map_iff, instIsLEObjTruncLT, triangleLTLTGELT_map_hom₁, isIso_truncLT_map_truncLTι_app, triangleLTLTGELT_obj_obj₃, truncLEIsoTruncLT_hom_ι, truncLEIsoTruncLT_inv_ι_app, natTransTruncLTOfLE_refl, triangleLTLTGELT_obj_mor₃, instIsGEObjTruncLT, isZero_truncLT_obj_of_isGE, eTruncLT_obj_coe, isLE_truncLT_obj, triangleLTGE_map_hom₃, liftTruncLT_aux, natTransTruncLTOfLE_ι_app_assoc, truncLT_map_truncLTι_app_assoc, natTransTruncLTOfLE_trans_app, triangleLTLTGELT_map_hom₂, triangleLTGE_map_hom₂, triangleLTGE_obj_mor₃, truncLEIsoTruncLT_inv_ι_assoc, truncGEδLT_comp_natTransTruncLTOfLE_app, liftTruncLT_ι_assoc, triangleLTGE_obj_obj₁, liftTruncLT_ι, triangleLTLTGELT_map_hom₃, truncLTι_comp_truncGEπ_app_assoc, truncGEδLT_comp_truncLTι_assoc, isGE_iff_isZero_truncLT_obj, isIso₁_truncLT_map_of_isGE, truncLEIsoTruncLT_inv_ι, truncLEIsoTruncLT_hom_ι_app_assoc, truncGEπ_comp_truncGEδLT, truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE_assoc, truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE, triangleLTLTGELT_obj_obj₂, natTransTruncLTOfLE_ι, isLE_iff_isIso_truncLTι_app, triangleLTGE_map_hom₁, truncLTι_comp_truncGEπ, truncGEδLT_comp_truncLTι_app_assoc, truncGELTδLT_app, truncLEIsoTruncLT_hom_ι_app, truncGEπ_comp_truncGEδLT_app, natTransTruncLTOfLE_ι_app, truncGELTToLTGE_app_pentagon, instIsIsoAppTruncLTιObjTruncGETruncLT, truncGEδLT_comp_natTransTruncLTOfLE_app_assoc, truncLTι_comp_truncGEπ_app, natTransTruncLTOfLE_refl_app, truncLEIsoTruncLT_inv_ι_app_assoc, instIsLEObjTruncLTHAddIntOfNat, triangleLTLTGELT_obj_mor₁, truncLT_map_truncGE_map_truncLTι_app_fac, instAdditiveTruncLT, natTransTruncLTOfLE_ι_assoc
truncLTGE 📖	CompOp	8 math math: truncLT_map_truncGE_map_truncLTι_app_fac_assoc, truncGELTToLTGE_app_pentagon_assoc, instIsLEObjTruncLTGEHSubIntOfNat, instIsIsoFunctorTruncGELTToLTGE, truncGELTToLTGE_app_pentagon_uniqueness, instIsGEObjTruncLTGE, truncGELTToLTGE_app_pentagon, truncLT_map_truncGE_map_truncLTι_app_fac
truncLTι 📖	CompOp	43 math math: truncGEδLT_comp_truncLTι, instIsIsoMapTruncLTTruncGEAppTruncLTι, truncLT_map_truncGE_map_truncLTι_app_fac_assoc, instIsIsoMapTruncLTAppTruncLTι, eTruncLT_ι_coe, truncLEIsoTruncLT_hom_ι_assoc, truncLT_map_truncLTι_app, triangleLTGE_obj_mor₁, truncGELTToLTGE_app_pentagon_assoc, truncGEδLT_comp_truncLTι_app, truncLTι_comp_truncGEπ_assoc, isIso_truncLT_map_iff, isIso_truncLT_map_truncLTι_app, truncLEIsoTruncLT_hom_ι, truncLEIsoTruncLT_inv_ι_app, triangleLTLTGELT_obj_mor₃, triangleLTGE_map_hom₃, liftTruncLT_aux, natTransTruncLTOfLE_ι_app_assoc, truncLT_map_truncLTι_app_assoc, triangleLTGE_map_hom₂, truncLEIsoTruncLT_inv_ι_assoc, liftTruncLT_ι_assoc, liftTruncLT_ι, truncLTι_comp_truncGEπ_app_assoc, truncGEδLT_comp_truncLTι_assoc, truncLEIsoTruncLT_inv_ι, truncLEIsoTruncLT_hom_ι_app_assoc, natTransTruncLTOfLE_ι, isLE_iff_isIso_truncLTι_app, triangleLTGE_map_hom₁, truncLTι_comp_truncGEπ, truncGEδLT_comp_truncLTι_app_assoc, truncGELTδLT_app, truncLEIsoTruncLT_hom_ι_app, natTransTruncLTOfLE_ι_app, truncGELTToLTGE_app_pentagon, instIsIsoAppTruncLTιObjTruncGETruncLT, truncLTι_comp_truncGEπ_app, truncLEIsoTruncLT_inv_ι_app_assoc, truncLT_map_truncGE_map_truncLTι_app_fac, natTransTruncLTOfLE_ι_assoc, eTruncLT_map_eq_truncLTι

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
descTruncGE_aux 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncGE CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.id CategoryTheory.NatTrans.app truncGEπ	—	CategoryTheory.Pretriangulated.Triangle.yoneda_exact₂ triangleLTGE_distinguished zero_of_isLE_of_isGE instIsLEObjTruncLTHSubIntOfNat
from_truncGE_obj_ext 📖	—	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id truncGE CategoryTheory.NatTrans.app truncGEπ	—	—	CategoryTheory.Pretriangulated.Triangle.yoneda_exact₃ triangleLTGE_distinguished zero_of_isLE_of_isGE isLE_shift instIsLEObj₁ObjTriangleTriangleLTGEHSubIntOfNat CategoryTheory.Limits.comp_zero sub_eq_zero CategoryTheory.Preadditive.comp_sub sub_self
instAdditiveTruncGE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.Additive truncGE	—	CategoryTheory.Functor.map_add
instAdditiveTruncLT 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.Additive truncLT	—	CategoryTheory.Functor.map_add
instIsGEObjTruncGE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE CategoryTheory.Functor.obj truncGE	—	isGE_truncGE_obj
instIsGEObjTruncGELT 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE CategoryTheory.Functor.obj truncGELT	—	instIsGEObjTruncGE
instIsGEObjTruncGE_1 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE CategoryTheory.Functor.obj truncGE	—	isGE_truncGE_obj isGE_of_ge isGE_of_iso instIsIsoAppTruncGEπOfIsGE
instIsGEObjTruncLT 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE CategoryTheory.Functor.obj truncLT	—	isGE_iff_isZero_truncLT_obj isIso₁_truncLT_map_of_isGE triangleLTGE_distinguished instIsGEObjTruncGE_1 CategoryTheory.Limits.IsZero.of_iso
instIsGEObjTruncLTGE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE CategoryTheory.Functor.obj truncLTGE	—	instIsGEObjTruncLT instIsGEObjTruncGE
instIsGEObj₃ObjTriangleTriangleLTGE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTGE	—	instIsGEObjTruncGE
instIsGEOfNat 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE CategoryTheory.Limits.HasZeroObject.zero'	—	isGE_of_isZero CategoryTheory.Limits.isZero_zero
instIsIsoAppTruncGEπOfIsGE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.id truncGE CategoryTheory.NatTrans.app truncGEπ	—	isGE_iff_isIso_truncGEπ_app
instIsIsoAppTruncLTιObjTruncGETruncLT 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.IsIso CategoryTheory.Functor.obj truncLT truncGE CategoryTheory.Functor.id CategoryTheory.NatTrans.app truncLTι	—	isLE_iff_isIso_truncLTι_app instIsLEObjTruncGE instIsLEObjTruncLTHSubIntOfNat
instIsIsoFunctorTruncGELTToLTGE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.Functor.category truncGELT truncLTGE truncGELTToLTGE	—	CategoryTheory.NatTrans.isIso_iff_isIso_app natTransTruncLTOfLE_ι_app triangleLTLTGELT_distinguished triangleLTGE_distinguished isIso₁_truncLT_map_of_isGE CategoryTheory.Triangulated.Octahedron.mem instIsGEObjTruncGE instIsLEObjTruncGELTHSubIntOfNat to_truncLT_obj_ext from_truncGE_obj_ext liftTruncLT_ι truncGELTToLTGE_app_pentagon CategoryTheory.Triangulated.Octahedron.comm₁ CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality instIsLEObjTruncLTHSubIntOfNat CategoryTheory.IsIso.of_isIso_fac_left instIsIsoAppTruncLTιObjTruncGETruncLT CategoryTheory.Limits.IsZero.eq_of_src isZero instIsGEObjTruncGELT instIsLEObjTruncLTGEHSubIntOfNat instIsGEObjTruncLTGE
instIsIsoMapTruncGEAppTruncGEπ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.IsIso CategoryTheory.Functor.obj truncGE CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app truncGEπ	—	isIso_truncGE_map_truncGEπ_app le_refl
instIsIsoMapTruncLTAppTruncLTι 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.IsIso CategoryTheory.Functor.obj truncLT CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app truncLTι	—	isIso_truncLT_map_truncLTι_app le_refl
instIsIsoMapTruncLTTruncGEAppTruncLTι 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.IsIso CategoryTheory.Functor.obj truncLT truncGE CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app truncLTι	—	truncLT_map_truncGE_map_truncLTι_app_fac CategoryTheory.IsIso.comp_isIso instIsIsoAppTruncLTιObjTruncGETruncLT CategoryTheory.NatIso.isIso_app_of_isIso instIsIsoFunctorTruncGELTToLTGE
instIsLEObjTruncGE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE CategoryTheory.Functor.obj truncGE	—	isLE_iff_isZero_truncGE_obj isIso₂_truncGE_map_of_isLE triangleLTGE_distinguished instIsLEObjTruncLT CategoryTheory.Limits.IsZero.of_iso
instIsLEObjTruncGELTHSubIntOfNat 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE CategoryTheory.Functor.obj truncGELT	—	instIsLEObjTruncGE instIsLEObjTruncLTHSubIntOfNat
instIsLEObjTruncLT 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE CategoryTheory.Functor.obj truncLT	—	isLE_truncLT_obj isLE_iff_isIso_truncLTι_app isLE_of_le isLE_of_iso
instIsLEObjTruncLTGEHSubIntOfNat 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE CategoryTheory.Functor.obj truncLTGE	—	instIsLEObjTruncLTHSubIntOfNat
instIsLEObjTruncLTHAddIntOfNat 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE CategoryTheory.Functor.obj truncLT	—	isLE_truncLT_obj
instIsLEObjTruncLTHSubIntOfNat 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE CategoryTheory.Functor.obj truncLT	—	isLE_truncLT_obj
instIsLEObj₁ObjTriangleTriangleLTGEHSubIntOfNat 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTGE	—	instIsLEObjTruncLTHSubIntOfNat
instIsLEOfNat 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE CategoryTheory.Limits.HasZeroObject.zero'	—	isLE_of_isZero CategoryTheory.Limits.isZero_zero
instIsTriangulatedBounded 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty.IsTriangulated bounded	—	CategoryTheory.ObjectProperty.instIsTriangulatedMinOfIsClosedUnderIsomorphisms instIsTriangulatedPlus instIsClosedUnderIsomorphismsPlus instIsTriangulatedMinus
instIsTriangulatedMinus 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty.IsTriangulated minus	—	CategoryTheory.ObjectProperty.IsTriangulatedClosed₂.mk' instIsClosedUnderIsomorphismsMinus isLE₂ isLE_of_le le_max_left le_max_right CategoryTheory.Limits.isZero_zero instIsLEOfNat instIsStableUnderShiftMinusInt
instIsTriangulatedPlus 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty.IsTriangulated plus	—	CategoryTheory.ObjectProperty.IsTriangulatedClosed₂.mk' instIsClosedUnderIsomorphismsPlus isGE₂ isGE_of_ge min_le_left min_le_right CategoryTheory.Limits.isZero_zero instIsGEOfNat instIsStableUnderShiftPlusInt
isGE_iff_isIso_truncGEπ_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.id truncGE CategoryTheory.NatTrans.app truncGEπ	—	triangle_iso_exists CategoryTheory.Pretriangulated.inv_rot_of_distTriang CategoryTheory.Pretriangulated.contractible_distinguished triangleLTGE_distinguished isLE_of_iso CategoryTheory.Functor.preservesZeroMorphisms_of_additive instIsLEOfNat instIsLEObjTruncLTHSubIntOfNat instIsGEObjTruncGE CategoryTheory.Pretriangulated.TriangleMorphism.comm₂ CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Pretriangulated.Triangle.instIsIsoHom₂ CategoryTheory.Iso.isIso_hom CategoryTheory.Pretriangulated.Triangle.instIsIsoHom₃ isGE_of_iso
isGE_iff_isZero_truncLT_obj 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj truncLT	—	isGE_iff_isIso_truncGEπ_app CategoryTheory.Pretriangulated.Triangle.isZero₁_iff_isIso₂ triangleLTGE_distinguished
isGE_iff_orthogonal 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	zero isGE_iff_isZero_truncLT_obj CategoryTheory.Limits.IsZero.iff_id_eq_zero to_truncLT_obj_ext CategoryTheory.Category.id_comp CategoryTheory.Limits.zero_comp instIsLEObjTruncLTHAddIntOfNat instIsLEObjTruncLTHSubIntOfNat
isGE_of_isZero 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Limits.IsZero	IsGE	—	isGE_of_iso CategoryTheory.Functor.map_isZero CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditiveTruncGE instIsGEObjTruncGE
isGE_truncGE_obj 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE CategoryTheory.Functor.obj truncGE	—	isGE_of_ge
isGE₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	IsGE CategoryTheory.Pretriangulated.Triangle.obj₂	—	isGE_iff_orthogonal CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂ zero CategoryTheory.Limits.zero_comp
isIso_truncGE_map_iff 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.IsIso CategoryTheory.Functor.obj truncGE 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 truncGEπ IsLE	—	CategoryTheory.Pretriangulated.isomorphic_distinguished triangleLTGE_distinguished CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp truncGEπ_naturality CategoryTheory.Functor.map_id CategoryTheory.IsIso.hom_inv_id_assoc instIsLEObjTruncLTHAddIntOfNat triangle_iso_exists instIsGEObjTruncGE from_truncGE_obj_ext CategoryTheory.Pretriangulated.TriangleMorphism.comm₂ CategoryTheory.Pretriangulated.Triangle.instIsIsoHom₃ CategoryTheory.Iso.isIso_hom
isIso_truncGE_map_truncGEπ_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.IsIso CategoryTheory.Functor.obj truncGE CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app truncGEπ	—	isIso₂_truncGE_map_of_isLE triangleLTGE_distinguished isLE_truncLT_obj sub_add_cancel
isIso_truncLT_map_iff 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.IsIso CategoryTheory.Functor.obj truncLT 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 truncLTι IsGE	—	CategoryTheory.Pretriangulated.isomorphic_distinguished triangleLTGE_distinguished CategoryTheory.Category.comp_id CategoryTheory.NatTrans.naturality CategoryTheory.Category.id_comp CategoryTheory.Functor.map_isIso CategoryTheory.Functor.map_inv CategoryTheory.Category.assoc CategoryTheory.IsIso.inv_hom_id instIsGEObjTruncGE triangle_iso_exists instIsLEObjTruncLTHSubIntOfNat to_truncLT_obj_ext CategoryTheory.Pretriangulated.TriangleMorphism.comm₁ CategoryTheory.Pretriangulated.Triangle.instIsIsoHom₁ CategoryTheory.Iso.isIso_hom
isIso_truncLT_map_truncLTι_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.IsIso CategoryTheory.Functor.obj truncLT CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app truncLTι	—	isIso₁_truncLT_map_of_isGE triangleLTGE_distinguished isGE_of_ge instIsGEObjTruncGE
isIso₁_truncLT_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 truncLT CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle.mor₁	—	isIso_truncLT_map_iff CategoryTheory.Pretriangulated.distinguished_cocone_triangle triangleLTGE_distinguished isGE₂ CategoryTheory.Triangulated.Octahedron.mem instIsGEObjTruncGE
isIso₂_truncGE_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 truncGE CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle.mor₂	—	isIso_truncGE_map_iff CategoryTheory.Pretriangulated.distinguished_cocone_triangle₁ CategoryTheory.Pretriangulated.rot_of_distTriang triangleLTGE_distinguished isLE₂ CategoryTheory.Triangulated.Octahedron.mem isLE_shift instIsLEObjTruncLTHAddIntOfNat isLE_of_shift
isLE_iff_isIso_truncLTι_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE CategoryTheory.IsIso CategoryTheory.Functor.obj truncLT CategoryTheory.Functor.id CategoryTheory.NatTrans.app truncLTι	—	triangle_iso_exists CategoryTheory.Pretriangulated.contractible_distinguished triangleLTGE_distinguished instIsGEOfNat instIsLEObjTruncLTHAddIntOfNat instIsGEObjTruncGE CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Pretriangulated.Triangle.instIsIsoHom₂ CategoryTheory.Iso.isIso_hom CategoryTheory.Pretriangulated.comp_hom₂ CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.Pretriangulated.TriangleMorphism.comm₁ CategoryTheory.Pretriangulated.Triangle.instIsIsoHom₁ CategoryTheory.Iso.isIso_inv isLE_of_iso
isLE_iff_isZero_truncGE_obj 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj truncGE	—	isLE_iff_isIso_truncLTι_app CategoryTheory.Pretriangulated.Triangle.isZero₃_iff_isIso₁ triangleLTGE_distinguished
isLE_iff_orthogonal 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	zero isLE_iff_isZero_truncGE_obj CategoryTheory.Limits.IsZero.iff_id_eq_zero from_truncGE_obj_ext CategoryTheory.Category.comp_id CategoryTheory.Limits.comp_zero instIsGEObjTruncGE
isLE_of_isZero 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Limits.IsZero	IsLE	—	isLE_of_iso CategoryTheory.Functor.map_isZero CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditiveTruncLT instIsLEObjTruncLTHAddIntOfNat
isLE_truncLT_obj 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE CategoryTheory.Functor.obj truncLT	—	isLE_of_le
isLE₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	IsLE CategoryTheory.Pretriangulated.Triangle.obj₂	—	isLE_iff_orthogonal CategoryTheory.Pretriangulated.Triangle.yoneda_exact₂ zero CategoryTheory.Limits.comp_zero
isZero_truncGE_obj_of_isLE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj truncGE	—	isLE_iff_isZero_truncGE_obj
isZero_truncLT_obj_of_isGE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj truncLT	—	isGE_iff_isZero_truncLT_obj
liftTruncLT_aux 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncLT CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.id CategoryTheory.NatTrans.app truncLTι	—	CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂ triangleLTGE_distinguished zero_of_isLE_of_isGE instIsGEObjTruncGE
liftTruncLT_ι 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncLT CategoryTheory.Functor.id liftTruncLT CategoryTheory.NatTrans.app truncLTι	—	liftTruncLT_aux
liftTruncLT_ι_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncLT liftTruncLT CategoryTheory.NatTrans.app CategoryTheory.Functor.id truncLTι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' liftTruncLT_ι
natTransTriangleLTGEOfLE_refl 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	natTransTriangleLTGEOfLE CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category triangleLTGE	—	—
natTransTriangleLTGEOfLE_trans 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category triangleLTGE natTransTriangleLTGEOfLE LE.le.trans PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	—	—
natTransTruncGEOfLE_refl 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	natTransTruncGEOfLE CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category truncGE	—	natTransTriangleLTGEOfLE_refl
natTransTruncGEOfLE_refl_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.NatTrans.app truncGE natTransTruncGEOfLE CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	CategoryTheory.congr_app natTransTruncGEOfLE_refl
natTransTruncGEOfLE_trans 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category truncGE natTransTruncGEOfLE LE.le.trans PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	—	LE.le.trans natTransTriangleLTGEOfLE_trans
natTransTruncGEOfLE_trans_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncGE CategoryTheory.NatTrans.app natTransTruncGEOfLE LE.le.trans PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	—	CategoryTheory.congr_app LE.le.trans natTransTruncGEOfLE_trans
natTransTruncLTOfLE_refl 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	natTransTruncLTOfLE CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category truncLT	—	natTransTriangleLTGEOfLE_refl
natTransTruncLTOfLE_refl_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.NatTrans.app truncLT natTransTruncLTOfLE CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	CategoryTheory.congr_app natTransTruncLTOfLE_refl
natTransTruncLTOfLE_trans 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category truncLT natTransTruncLTOfLE LE.le.trans PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	—	LE.le.trans natTransTriangleLTGEOfLE_trans
natTransTruncLTOfLE_trans_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncLT CategoryTheory.NatTrans.app natTransTruncLTOfLE LE.le.trans PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	—	CategoryTheory.congr_app LE.le.trans natTransTruncLTOfLE_trans
natTransTruncLTOfLE_ι 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category truncLT CategoryTheory.Functor.id natTransTruncLTOfLE truncLTι	—	CategoryTheory.NatTrans.ext' natTransTruncLTOfLE_ι_app
natTransTruncLTOfLE_ι_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncLT CategoryTheory.Functor.id CategoryTheory.NatTrans.app natTransTruncLTOfLE truncLTι	—	CategoryTheory.Category.comp_id CategoryTheory.Pretriangulated.TriangleMorphism.comm₁
natTransTruncLTOfLE_ι_app_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncLT CategoryTheory.NatTrans.app natTransTruncLTOfLE CategoryTheory.Functor.id truncLTι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' natTransTruncLTOfLE_ι_app
natTransTruncLTOfLE_ι_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category truncLT natTransTruncLTOfLE CategoryTheory.Functor.id truncLTι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' natTransTruncLTOfLE_ι
to_truncLT_obj_ext 📖	—	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncLT CategoryTheory.Functor.id CategoryTheory.NatTrans.app truncLTι	—	—	CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂ CategoryTheory.Pretriangulated.inv_rot_of_distTriang triangleLTGE_distinguished zero_of_isLE_of_isGE isGE_shift instIsGEObjTruncGE CategoryTheory.Limits.zero_comp sub_eq_zero CategoryTheory.Preadditive.sub_comp sub_self
triangleLTGE_distinguished 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.triangleCategory triangleLTGE	—	—
triangleLTGE_map_hom₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ CategoryTheory.Functor.obj truncLT CategoryTheory.Functor.id truncGE CategoryTheory.NatTrans.app truncLTι truncGEπ CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid truncGEδLT CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTGE	—	—
triangleLTGE_map_hom₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ CategoryTheory.Functor.obj truncLT CategoryTheory.Functor.id truncGE CategoryTheory.NatTrans.app truncLTι truncGEπ CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid truncGEδLT CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTGE	—	—
triangleLTGE_map_hom₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ CategoryTheory.Functor.obj truncLT CategoryTheory.Functor.id truncGE CategoryTheory.NatTrans.app truncLTι truncGEπ CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid truncGEδLT CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTGE	—	—
triangleLTGE_obj_mor₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.mor₁ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTGE CategoryTheory.NatTrans.app truncLT CategoryTheory.Functor.id truncLTι	—	—
triangleLTGE_obj_mor₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.mor₂ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTGE CategoryTheory.NatTrans.app CategoryTheory.Functor.id truncGE truncGEπ	—	—
triangleLTGE_obj_mor₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTGE CategoryTheory.NatTrans.app truncGE CategoryTheory.Functor.comp truncLT CategoryTheory.shiftFunctor Int.instAddMonoid truncGEδLT	—	—
triangleLTGE_obj_obj₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTGE truncLT	—	—
triangleLTGE_obj_obj₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTGE	—	—
triangleLTGE_obj_obj₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTGE truncGE	—	—
triangleLTLTGELT_distinguished 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.triangleCategory triangleLTLTGELT	—	isIso_truncLT_map_truncLTι_app CategoryTheory.Pretriangulated.isomorphic_distinguished triangleLTGE_distinguished CategoryTheory.Category.comp_id to_truncLT_obj_ext CategoryTheory.NatTrans.naturality CategoryTheory.Category.assoc natTransTruncLTOfLE_ι_app_assoc instIsLEObjTruncLT instIsLEObjTruncLTHSubIntOfNat CategoryTheory.Category.id_comp CategoryTheory.Functor.map_isIso CategoryTheory.Functor.map_inv CategoryTheory.IsIso.hom_inv_id
triangleLTLTGELT_map_hom₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ CategoryTheory.Functor.obj truncLT CategoryTheory.Functor.comp truncGE CategoryTheory.NatTrans.app natTransTruncLTOfLE CategoryTheory.Functor.whiskerLeft CategoryTheory.Functor.id truncGEπ CategoryTheory.shiftFunctor Int.instAddMonoid truncGELTδLT CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTLTGELT	—	—
triangleLTLTGELT_map_hom₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ CategoryTheory.Functor.obj truncLT CategoryTheory.Functor.comp truncGE CategoryTheory.NatTrans.app natTransTruncLTOfLE CategoryTheory.Functor.whiskerLeft CategoryTheory.Functor.id truncGEπ CategoryTheory.shiftFunctor Int.instAddMonoid truncGELTδLT CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTLTGELT	—	—
triangleLTLTGELT_map_hom₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ CategoryTheory.Functor.obj truncLT CategoryTheory.Functor.comp truncGE CategoryTheory.NatTrans.app natTransTruncLTOfLE CategoryTheory.Functor.whiskerLeft CategoryTheory.Functor.id truncGEπ CategoryTheory.shiftFunctor Int.instAddMonoid truncGELTδLT CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTLTGELT	—	—
triangleLTLTGELT_obj_mor₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.mor₁ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTLTGELT CategoryTheory.NatTrans.app truncLT natTransTruncLTOfLE	—	—
triangleLTLTGELT_obj_mor₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.mor₂ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTLTGELT CategoryTheory.NatTrans.app CategoryTheory.Functor.id truncGE truncGEπ truncLT	—	—
triangleLTLTGELT_obj_mor₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTLTGELT CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct truncGE truncLT CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.NatTrans.app CategoryTheory.Functor.comp truncGEδLT CategoryTheory.Functor.map CategoryTheory.Functor.id truncLTι	—	—
triangleLTLTGELT_obj_obj₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTLTGELT truncLT	—	—
triangleLTLTGELT_obj_obj₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTLTGELT truncLT	—	—
triangleLTLTGELT_obj_obj₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory triangleLTLTGELT truncGE truncLT	—	—
triangle_iso_exists 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	CategoryTheory.Iso CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ CategoryTheory.Iso.hom CategoryTheory.Pretriangulated.Triangle.obj₂	—	triangle_map_exists triangle_map_ext CategoryTheory.Iso.hom_inv_id CategoryTheory.Iso.inv_hom_id
triangle_map_exists 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	Quiver.Hom CategoryTheory.Pretriangulated.Triangle CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Pretriangulated.TriangleMorphism.hom₂	—	CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂ zero CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism
triangle_map_ext 📖	—	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.TriangleMorphism.hom₂	—	—	CategoryTheory.Pretriangulated.Triangle.hom_ext CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂ CategoryTheory.Pretriangulated.inv_rot_of_distTriang CategoryTheory.Pretriangulated.TriangleMorphism.comm₁ CategoryTheory.Limits.comp_zero add_neg_cancel zero_of_isLE_of_isGE isGE_shift CategoryTheory.Preadditive.comp_neg CategoryTheory.Limits.zero_comp neg_zero CategoryTheory.Pretriangulated.Triangle.yoneda_exact₃ CategoryTheory.Pretriangulated.TriangleMorphism.comm₂ isLE_shift sub_eq_zero sub_self
truncGELTToLTGE_app_pentagon 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id truncLT truncGE CategoryTheory.NatTrans.app truncGEπ truncLTGE truncGELT truncGELTToLTGE truncLTι	—	instIsGEObjTruncGE liftTruncLT_ι π_descTruncGE
truncGELTToLTGE_app_pentagon_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncLT truncGE CategoryTheory.NatTrans.app CategoryTheory.Functor.id truncGEπ truncGELT truncLTGE truncGELTToLTGE truncLTι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' truncGELTToLTGE_app_pentagon
truncGELTToLTGE_app_pentagon_uniqueness 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id truncLT truncGE CategoryTheory.NatTrans.app truncGEπ truncLTGE truncLTι	CategoryTheory.NatTrans.app truncGELT truncLTGE truncGELTToLTGE	—	to_truncLT_obj_ext from_truncGE_obj_ext truncGELTToLTGE_app_pentagon instIsGEObjTruncGE instIsLEObjTruncGELTHSubIntOfNat
truncGELTδLT_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.NatTrans.app truncGELT CategoryTheory.Functor.comp truncLT CategoryTheory.shiftFunctor Int.instAddMonoid truncGELTδLT CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncGE truncGEδLT CategoryTheory.Functor.map CategoryTheory.Functor.id truncLTι	—	—
truncGE_map_truncGEπ_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.map truncGE CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.NatTrans.app truncGEπ	—	from_truncGE_obj_ext truncGEπ_naturality instIsGEObjTruncGE
truncGE_map_truncGEπ_app_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncGE CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.id truncGEπ	—	Mathlib.Tactic.Reassoc.eq_whisker' truncGE_map_truncGEπ_app
truncGEδLT_comp_natTransTruncLTOfLE_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncGE CategoryTheory.Functor.comp truncLT CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.NatTrans.app truncGEδLT CategoryTheory.Functor.map natTransTruncLTOfLE natTransTruncGEOfLE	—	CategoryTheory.Pretriangulated.TriangleMorphism.comm₃
truncGEδLT_comp_natTransTruncLTOfLE_app_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncGE CategoryTheory.shiftFunctor Int.instAddMonoid truncLT CategoryTheory.NatTrans.app CategoryTheory.Functor.comp truncGEδLT CategoryTheory.Functor.map natTransTruncLTOfLE natTransTruncGEOfLE	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' truncGEδLT_comp_natTransTruncLTOfLE_app
truncGEδLT_comp_truncLTι 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category truncGE CategoryTheory.Functor.comp truncLT CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Functor.id truncGEδLT CategoryTheory.Functor.whiskerRight truncLTι Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.instZeroHomFunctor	—	CategoryTheory.NatTrans.ext' truncGEδLT_comp_truncLTι_app
truncGEδLT_comp_truncLTι_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncGE CategoryTheory.Functor.comp truncLT CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Functor.id CategoryTheory.NatTrans.app truncGEδLT CategoryTheory.Functor.map truncLTι Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁ triangleLTGE_distinguished
truncGEδLT_comp_truncLTι_app_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncGE CategoryTheory.shiftFunctor Int.instAddMonoid truncLT CategoryTheory.NatTrans.app CategoryTheory.Functor.comp truncGEδLT CategoryTheory.Functor.map CategoryTheory.Functor.id truncLTι Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' truncGEδLT_comp_truncLTι_app
truncGEδLT_comp_truncLTι_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category truncGE CategoryTheory.Functor.comp truncLT CategoryTheory.shiftFunctor Int.instAddMonoid truncGEδLT CategoryTheory.Functor.id CategoryTheory.Functor.whiskerRight truncLTι Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.instZeroHomFunctor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' truncGEδLT_comp_truncLTι
truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category truncGE CategoryTheory.Functor.comp truncLT CategoryTheory.shiftFunctor Int.instAddMonoid truncGEδLT CategoryTheory.Functor.whiskerRight natTransTruncLTOfLE natTransTruncGEOfLE	—	CategoryTheory.NatTrans.ext' truncGEδLT_comp_natTransTruncLTOfLE_app
truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category truncGE CategoryTheory.Functor.comp truncLT CategoryTheory.shiftFunctor Int.instAddMonoid truncGEδLT CategoryTheory.Functor.whiskerRight natTransTruncLTOfLE natTransTruncGEOfLE	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE
truncGEπ_comp_truncGEδLT 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id truncGE CategoryTheory.Functor.comp truncLT CategoryTheory.shiftFunctor Int.instAddMonoid truncGEπ truncGEδLT Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.instZeroHomFunctor	—	CategoryTheory.NatTrans.ext' truncGEπ_comp_truncGEδLT_app
truncGEπ_comp_truncGEδLT_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id truncGE CategoryTheory.Functor.comp truncLT CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.NatTrans.app truncGEπ truncGEδLT Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃ triangleLTGE_distinguished
truncGEπ_comp_truncGEδLT_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π CategoryTheory.shiftFunctor Int.instAddMonoid truncLT CategoryTheory.Functor.comp truncGEδLT Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' truncGEπ_comp_truncGEδLT_app
truncGEπ_comp_truncGEδLT_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π CategoryTheory.Functor.comp truncLT CategoryTheory.shiftFunctor Int.instAddMonoid truncGEδLT Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.instZeroHomFunctor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' truncGEπ_comp_truncGEδLT
truncGEπ_naturality 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id truncGE CategoryTheory.NatTrans.app truncGEπ CategoryTheory.Functor.map	—	CategoryTheory.NatTrans.naturality
truncGEπ_naturality_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π CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' truncGEπ_naturality
truncLT_map_truncGE_map_truncLTι_app_fac 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncLT truncGE CategoryTheory.Functor.id truncLTGE CategoryTheory.NatTrans.app truncLTι truncGELT truncGELTToLTGE CategoryTheory.Functor.map	—	instIsIsoAppTruncLTιObjTruncGETruncLT CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.IsIso.inv_isIso CategoryTheory.IsIso.inv_hom_id_assoc truncGELTToLTGE_app_pentagon_uniqueness CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality truncGEπ_naturality
truncLT_map_truncGE_map_truncLTι_app_fac_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncLT truncGE CategoryTheory.NatTrans.app CategoryTheory.Functor.id truncLTι truncGELT truncLTGE truncGELTToLTGE CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' truncLT_map_truncGE_map_truncLTι_app_fac
truncLT_map_truncLTι_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.map truncLT CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.NatTrans.app truncLTι	—	to_truncLT_obj_ext CategoryTheory.NatTrans.naturality instIsLEObjTruncLTHSubIntOfNat
truncLT_map_truncLTι_app_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncLT CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.id truncLTι	—	Mathlib.Tactic.Reassoc.eq_whisker' truncLT_map_truncLTι_app
truncLTι_comp_truncGEπ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category truncLT CategoryTheory.Functor.id truncGE truncLTι truncGEπ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.instZeroHomFunctor	—	CategoryTheory.NatTrans.ext' truncLTι_comp_truncGEπ_app
truncLTι_comp_truncGEπ_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncLT CategoryTheory.Functor.id truncGE CategoryTheory.NatTrans.app truncLTι truncGEπ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂ triangleLTGE_distinguished
truncLTι_comp_truncGEπ_app_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj truncLT CategoryTheory.NatTrans.app CategoryTheory.Functor.id truncLTι truncGE truncGEπ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' truncLTι_comp_truncGEπ_app
truncLTι_comp_truncGEπ_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category truncLT CategoryTheory.Functor.id truncLTι truncGE truncGEπ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.instZeroHomFunctor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' truncLTι_comp_truncGEπ
π_descTruncGE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id truncGE CategoryTheory.NatTrans.app truncGEπ descTruncGE	—	descTruncGE_aux
π_descTruncGE_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π descTruncGE	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_descTruncGE
π_natTransTruncGEOfLE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id truncGE truncGEπ natTransTruncGEOfLE	—	CategoryTheory.NatTrans.ext' π_natTransTruncGEOfLE_app
π_natTransTruncGEOfLE_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id truncGE CategoryTheory.NatTrans.app truncGEπ natTransTruncGEOfLE	—	CategoryTheory.Category.id_comp CategoryTheory.Pretriangulated.TriangleMorphism.comm₂
π_natTransTruncGEOfLE_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π natTransTruncGEOfLE	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_natTransTruncGEOfLE_app
π_natTransTruncGEOfLE_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π natTransTruncGEOfLE	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_natTransTruncGEOfLE

---

← Back to Index