ETrunc

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

Statistics

Metric	Count
Definitions eTriangleLTGE, eTruncGE, eTruncGEIsoGEGE, eTruncGEToGEGE, eTruncGEδLT, eTruncGEπ, eTruncLT, eTruncLTGEIsoGELT, eTruncLTGELTSelfToGELT, eTruncLTGELTSelfToLTGE, eTruncLTLTIsoLT, eTruncLTLTToLT, eTruncLTι	13
Theorems eTriangleLTGE_distinguished, eTriangleLTGE_map_app_hom₁, eTriangleLTGE_map_app_hom₂, eTriangleLTGE_map_app_hom₃, eTriangleLTGE_obj_map_hom₁, eTriangleLTGE_obj_map_hom₂, eTriangleLTGE_obj_map_hom₃, eTriangleLTGE_obj_obj_mor₁, eTriangleLTGE_obj_obj_mor₂, eTriangleLTGE_obj_obj_mor₃, eTriangleLTGE_obj_obj_obj₁, eTriangleLTGE_obj_obj_obj₂, eTriangleLTGE_obj_obj_obj₃, eTruncGEIsoGEGE_hom, eTruncGEIsoGEGE_hom_inv_id_app, eTruncGEIsoGEGE_hom_inv_id_app_assoc, eTruncGEIsoGEGE_inv_hom_id_app, eTruncGEIsoGEGE_inv_hom_id_app_assoc, eTruncGEToGEGE_app, eTruncGE_obj_bot, eTruncGE_obj_coe, eTruncGE_obj_map_eTruncGEπ_app, eTruncGE_obj_map_eTruncGEπ_app_assoc, eTruncGE_obj_top, eTruncGEδLT_coe, eTruncGEπ_app_eTruncGE_map_app, eTruncGEπ_app_eTruncGE_map_app_assoc, eTruncGEπ_bot, eTruncGEπ_coe, eTruncGEπ_naturality, eTruncGEπ_naturality_assoc, eTruncGEπ_top, eTruncLTGEIsoGELT_hom_app_fac, eTruncLTGEIsoGELT_hom_app_fac', eTruncLTGEIsoGELT_hom_app_fac'_assoc, eTruncLTGEIsoGELT_hom_app_fac_assoc, eTruncLTGEIsoGELT_hom_naturality, eTruncLTGEIsoGELT_hom_naturality_assoc, eTruncLTGEIsoGELT_naturality_app, eTruncLTGEIsoGELT_naturality_app_assoc, eTruncLTGELTSelfToGELT_app, eTruncLTGELTSelfToLTGE_app, eTruncLTLTIsoLT_hom, eTruncLTLTIsoLT_hom_inv_id_app, eTruncLTLTIsoLT_hom_inv_id_app_assoc, eTruncLTLTIsoLT_inv_hom_id_app, eTruncLTLTIsoLT_inv_hom_id_app_assoc, eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_obj, eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_obj_assoc, eTruncLTLTToLT_app, eTruncLT_map_app_eTruncLTι_app, eTruncLT_map_app_eTruncLTι_app_assoc, eTruncLT_map_eq_truncLTι, eTruncLT_obj_bot, eTruncLT_obj_coe, eTruncLT_obj_map_eTruncLTι_app, eTruncLT_obj_map_eTruncLTι_app_assoc, eTruncLT_obj_map_eTruncLTι_app_eTruncLT_map_app, eTruncLT_obj_map_eTruncLTι_app_eTruncLT_map_app_assoc, eTruncLT_obj_top, eTruncLT_ι_bot, eTruncLT_ι_coe, eTruncLT_ι_top, eTruncLTι_naturality, eTruncLTι_naturality_assoc, instAdditiveObjEIntFunctorETruncGE, instAdditiveObjEIntFunctorETruncLT, instIsGEObjEIntFunctorETruncGE, instIsGEObjEIntFunctorETruncLT, instIsIsoAppETruncLTιObjEIntFunctorETruncLT, instIsIsoFunctorETruncGEπBotEInt, instIsIsoFunctorETruncLTGELTSelfToGELT, instIsIsoFunctorETruncLTGELTSelfToLTGE, instIsIsoFunctorETruncLTιTopEInt, instIsIsoMapObjEIntFunctorETruncLTAppETruncLTι, instIsLEObjEIntFunctorETruncGE, instIsLEObjEIntFunctorETruncLT, isGE_eTruncGE_obj_obj, isIso_eTruncGEIsoGEGE, isIso_eTruncGE_obj_map_truncGEπ_app, isIso_eTruncLTLTIsoLT, isIso_eTruncLT_obj_map_truncLTπ_app, isLE_eTruncLT_obj_obj, isZero_eTruncGE_obj_obj, isZero_eTruncLT_obj_obj	85
Total	98

CategoryTheory.Triangulated.TStructure

Definitions

Name	Category	Theorems
eTriangleLTGE 📖	CompOp	13 math math: eTriangleLTGE_map_app_hom₃, eTriangleLTGE_map_app_hom₂, eTriangleLTGE_obj_obj_obj₁, eTriangleLTGE_obj_obj_mor₁, eTriangleLTGE_map_app_hom₁, eTriangleLTGE_obj_map_hom₃, eTriangleLTGE_distinguished, eTriangleLTGE_obj_obj_mor₃, eTriangleLTGE_obj_obj_obj₂, eTriangleLTGE_obj_obj_obj₃, eTriangleLTGE_obj_map_hom₂, eTriangleLTGE_obj_map_hom₁, eTriangleLTGE_obj_obj_mor₂
eTruncGE 📖	CompOp	58 math math: eTriangleLTGE_map_app_hom₃, triangleω₁δ_obj_mor₁, eTriangleLTGE_map_app_hom₂, eTruncGEπ_naturality_assoc, triangleω₁δ_obj_obj₂, eTruncLTGELTSelfToLTGE_app, isIso_eTruncGE_obj_map_truncGEπ_app, triangleω₁δ_map_hom₁, eTruncGEIsoGEGE_hom_inv_id_app_assoc, triangleω₁δ_map_hom₂, ω₁_map, eTruncGEπ_naturality, isZero_eTruncGE_obj_obj, eTruncLTGEIsoGELT_hom_app_fac, instIsIsoFunctorETruncLTGELTSelfToGELT, eTruncGEIsoGEGE_inv_hom_id_app_assoc, triangleω₁δ_map_hom₃, instIsGEObjEIntFunctorETruncGE, eTruncGEπ_top, eTruncLTGEIsoGELT_hom_app_fac'_assoc, eTruncLTGEIsoGELT_hom_app_fac_assoc, eTruncGEπ_app_eTruncGE_map_app_assoc, eTriangleLTGE_map_app_hom₁, ω₁_obj, eTriangleLTGE_obj_map_hom₃, eTruncGE_obj_map_eTruncGEπ_app_assoc, eTruncLTGELTSelfToGELT_app, eTruncLTGEIsoGELT_naturality_app_assoc, eTruncGE_obj_map_eTruncGEπ_app, triangleω₁δ_obj_obj₁, eTruncGEIsoGEGE_hom_inv_id_app, eTruncGEIsoGEGE_hom, ω₁δ_app, triangleω₁δ_obj_mor₃, eTruncGEπ_app_eTruncGE_map_app, isIso_eTruncGEIsoGEGE, eTruncGEIsoGEGE_inv_hom_id_app, eTruncGE_obj_top, eTruncLTGEIsoGELT_hom_app_fac', instIsIsoFunctorETruncLTGELTSelfToLTGE, eTruncLTGEIsoGELT_naturality_app, instIsLEObjEIntFunctorETruncGE, instIsIsoFunctorETruncGEπBotEInt, eTriangleLTGE_obj_obj_mor₃, eTruncGE_obj_coe, triangleω₁δ_obj_mor₂, eTruncGEδLT_coe, instAdditiveObjEIntFunctorETruncGE, isGE_eTruncGE_obj_obj, eTruncLTGEIsoGELT_hom_naturality_assoc, eTruncGE_obj_bot, triangleω₁δ_obj_obj₃, eTriangleLTGE_obj_obj_obj₃, eTriangleLTGE_obj_map_hom₂, eTriangleLTGE_obj_map_hom₁, eTriangleLTGE_obj_obj_mor₂, eTruncLTGEIsoGELT_hom_naturality, eTruncGEToGEGE_app
eTruncGEIsoGEGE 📖	CompOp	5 math math: eTruncGEIsoGEGE_hom_inv_id_app_assoc, eTruncGEIsoGEGE_inv_hom_id_app_assoc, eTruncGEIsoGEGE_hom_inv_id_app, eTruncGEIsoGEGE_hom, eTruncGEIsoGEGE_inv_hom_id_app
eTruncGEToGEGE 📖	CompOp	3 math math: eTruncGEIsoGEGE_hom, isIso_eTruncGEIsoGEGE, eTruncGEToGEGE_app
eTruncGEδLT 📖	CompOp	10 math math: eTriangleLTGE_map_app_hom₃, eTriangleLTGE_map_app_hom₂, eTriangleLTGE_map_app_hom₁, eTriangleLTGE_obj_map_hom₃, ω₁δ_app, triangleω₁δ_obj_mor₃, eTriangleLTGE_obj_obj_mor₃, eTruncGEδLT_coe, eTriangleLTGE_obj_map_hom₂, eTriangleLTGE_obj_map_hom₁
eTruncGEπ 📖	CompOp	25 math math: eTriangleLTGE_map_app_hom₃, eTriangleLTGE_map_app_hom₂, eTruncGEπ_naturality_assoc, isIso_eTruncGE_obj_map_truncGEπ_app, eTruncGEπ_bot, eTruncGEIsoGEGE_hom_inv_id_app_assoc, eTruncGEπ_naturality, eTruncGEIsoGEGE_inv_hom_id_app_assoc, eTruncGEπ_top, eTruncGEπ_app_eTruncGE_map_app_assoc, eTriangleLTGE_map_app_hom₁, eTriangleLTGE_obj_map_hom₃, eTruncGE_obj_map_eTruncGEπ_app_assoc, eTruncGE_obj_map_eTruncGEπ_app, eTruncGEIsoGEGE_hom_inv_id_app, ω₁δ_app, triangleω₁δ_obj_mor₃, eTruncGEπ_app_eTruncGE_map_app, eTruncGEIsoGEGE_inv_hom_id_app, instIsIsoFunctorETruncGEπBotEInt, eTruncGEπ_coe, eTriangleLTGE_obj_map_hom₂, eTriangleLTGE_obj_map_hom₁, eTriangleLTGE_obj_obj_mor₂, eTruncGEToGEGE_app
eTruncLT 📖	CompOp	66 math math: eTruncLT_map_app_eTruncLTι_app, eTriangleLTGE_map_app_hom₃, triangleω₁δ_obj_mor₁, eTriangleLTGE_map_app_hom₂, triangleω₁δ_obj_obj₂, eTruncLTLTIsoLT_inv_hom_id_app, instIsIsoMapObjEIntFunctorETruncLTAppETruncLTι, eTruncLTGELTSelfToLTGE_app, eTruncLTLTToLT_app, triangleω₁δ_map_hom₁, instAdditiveObjEIntFunctorETruncLT, triangleω₁δ_map_hom₂, eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_obj, eTriangleLTGE_obj_obj_obj₁, ω₁_map, eTruncLTGEIsoGELT_hom_app_fac, instIsIsoFunctorETruncLTGELTSelfToGELT, eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_obj_assoc, eTriangleLTGE_obj_obj_mor₁, triangleω₁δ_map_hom₃, instIsIsoFunctorETruncLTιTopEInt, eTruncLTGEIsoGELT_hom_app_fac'_assoc, eTruncLTGEIsoGELT_hom_app_fac_assoc, eTruncLT_obj_coe, eTruncLTLTIsoLT_hom_inv_id_app, eTruncLT_obj_map_eTruncLTι_app, eTruncLTLTIsoLT_inv_hom_id_app_assoc, eTriangleLTGE_map_app_hom₁, eTruncLT_ι_top, eTruncLT_obj_bot, ω₁_obj, eTruncLTι_naturality, eTriangleLTGE_obj_map_hom₃, isIso_eTruncLT_obj_map_truncLTπ_app, eTruncLT_obj_map_eTruncLTι_app_assoc, isIso_eTruncLTLTIsoLT, eTruncLTGELTSelfToGELT_app, eTruncLTGEIsoGELT_naturality_app_assoc, isLE_eTruncLT_obj_obj, triangleω₁δ_obj_obj₁, eTruncLT_map_app_eTruncLTι_app_assoc, ω₁δ_app, triangleω₁δ_obj_mor₃, eTruncLTLTIsoLT_hom_inv_id_app_assoc, eTruncLTGEIsoGELT_hom_app_fac', instIsIsoFunctorETruncLTGELTSelfToLTGE, eTruncLTGEIsoGELT_naturality_app, eTruncLT_obj_map_eTruncLTι_app_eTruncLT_map_app_assoc, eTriangleLTGE_obj_obj_mor₃, eTruncLTι_naturality_assoc, isZero_eTruncLT_obj_obj, instIsGEObjEIntFunctorETruncLT, eTruncLT_ι_bot, triangleω₁δ_obj_mor₂, eTruncGEδLT_coe, instIsIsoAppETruncLTιObjEIntFunctorETruncLT, eTruncLT_obj_top, instIsLEObjEIntFunctorETruncLT, eTruncLTGEIsoGELT_hom_naturality_assoc, eTruncLT_obj_map_eTruncLTι_app_eTruncLT_map_app, triangleω₁δ_obj_obj₃, eTruncLTLTIsoLT_hom, eTriangleLTGE_obj_map_hom₂, eTriangleLTGE_obj_map_hom₁, eTruncLTGEIsoGELT_hom_naturality, eTruncLT_map_eq_truncLTι
eTruncLTGEIsoGELT 📖	CompOp	10 math math: eTruncLTGEIsoGELT_hom_app_fac, eTruncLTGEIsoGELT_hom_app_fac'_assoc, eTruncLTGEIsoGELT_hom_app_fac_assoc, eTruncLTGEIsoGELT_naturality_app_assoc, ω₁δ_app, triangleω₁δ_obj_mor₃, eTruncLTGEIsoGELT_hom_app_fac', eTruncLTGEIsoGELT_naturality_app, eTruncLTGEIsoGELT_hom_naturality_assoc, eTruncLTGEIsoGELT_hom_naturality
eTruncLTGELTSelfToGELT 📖	CompOp	2 math math: instIsIsoFunctorETruncLTGELTSelfToGELT, eTruncLTGELTSelfToGELT_app
eTruncLTGELTSelfToLTGE 📖	CompOp	2 math math: eTruncLTGELTSelfToLTGE_app, instIsIsoFunctorETruncLTGELTSelfToLTGE
eTruncLTLTIsoLT 📖	CompOp	7 math math: eTruncLTLTIsoLT_inv_hom_id_app, eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_obj, eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_obj_assoc, eTruncLTLTIsoLT_hom_inv_id_app, eTruncLTLTIsoLT_inv_hom_id_app_assoc, eTruncLTLTIsoLT_hom_inv_id_app_assoc, eTruncLTLTIsoLT_hom
eTruncLTLTToLT 📖	CompOp	3 math math: eTruncLTLTToLT_app, isIso_eTruncLTLTIsoLT, eTruncLTLTIsoLT_hom
eTruncLTι 📖	CompOp	37 math math: eTruncLT_map_app_eTruncLTι_app, eTriangleLTGE_map_app_hom₃, eTriangleLTGE_map_app_hom₂, eTruncLTLTIsoLT_inv_hom_id_app, instIsIsoMapObjEIntFunctorETruncLTAppETruncLTι, eTruncLT_ι_coe, eTruncLTGELTSelfToLTGE_app, eTruncLTLTToLT_app, eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_obj, eTruncLTGEIsoGELT_hom_app_fac, eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_obj_assoc, eTriangleLTGE_obj_obj_mor₁, instIsIsoFunctorETruncLTιTopEInt, eTruncLTGEIsoGELT_hom_app_fac'_assoc, eTruncLTGEIsoGELT_hom_app_fac_assoc, eTruncLTLTIsoLT_hom_inv_id_app, eTruncLT_obj_map_eTruncLTι_app, eTruncLTLTIsoLT_inv_hom_id_app_assoc, eTriangleLTGE_map_app_hom₁, eTruncLT_ι_top, eTruncLTι_naturality, eTriangleLTGE_obj_map_hom₃, isIso_eTruncLT_obj_map_truncLTπ_app, eTruncLT_obj_map_eTruncLTι_app_assoc, eTruncLTGELTSelfToGELT_app, eTruncLT_map_app_eTruncLTι_app_assoc, ω₁δ_app, triangleω₁δ_obj_mor₃, eTruncLTLTIsoLT_hom_inv_id_app_assoc, eTruncLTGEIsoGELT_hom_app_fac', eTruncLT_obj_map_eTruncLTι_app_eTruncLT_map_app_assoc, eTruncLTι_naturality_assoc, eTruncLT_ι_bot, instIsIsoAppETruncLTιObjEIntFunctorETruncLT, eTruncLT_obj_map_eTruncLTι_app_eTruncLT_map_app, eTriangleLTGE_obj_map_hom₂, eTriangleLTGE_obj_map_hom₁

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eTriangleLTGE_distinguished 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.triangleCategory EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTriangleLTGE	—	CategoryTheory.Pretriangulated.Triangle.distinguished_iff_of_isZero₁ CategoryTheory.Functor.zero_obj CategoryTheory.IsIso.id triangleLTGE_distinguished CategoryTheory.Pretriangulated.Triangle.distinguished_iff_of_isZero₃
eTriangleLTGE_map_app_hom₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Pretriangulated.Triangle.functorMk EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT CategoryTheory.Functor.id eTruncGE eTruncLTι eTruncGEπ CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.whiskeringRight CategoryTheory.shiftFunctor Int.instAddMonoid eTruncGEδLT CategoryTheory.Functor.map eTriangleLTGE CategoryTheory.Pretriangulated.Triangle.π₁	—	—
eTriangleLTGE_map_app_hom₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Pretriangulated.Triangle.functorMk EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT CategoryTheory.Functor.id eTruncGE eTruncLTι eTruncGEπ CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.whiskeringRight CategoryTheory.shiftFunctor Int.instAddMonoid eTruncGEδLT CategoryTheory.Functor.map eTriangleLTGE CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
eTriangleLTGE_map_app_hom₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Pretriangulated.Triangle.functorMk EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT CategoryTheory.Functor.id eTruncGE eTruncLTι eTruncGEπ CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.whiskeringRight CategoryTheory.shiftFunctor Int.instAddMonoid eTruncGEδLT CategoryTheory.Functor.map eTriangleLTGE CategoryTheory.Pretriangulated.Triangle.π₃	—	—
eTriangleLTGE_obj_map_hom₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT CategoryTheory.Functor.id eTruncGE CategoryTheory.NatTrans.app eTruncLTι eTruncGEπ CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Functor.whiskeringRight eTruncGEδLT CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory eTriangleLTGE	—	—
eTriangleLTGE_obj_map_hom₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT CategoryTheory.Functor.id eTruncGE CategoryTheory.NatTrans.app eTruncLTι eTruncGEπ CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Functor.whiskeringRight eTruncGEδLT CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory eTriangleLTGE	—	—
eTriangleLTGE_obj_map_hom₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT CategoryTheory.Functor.id eTruncGE CategoryTheory.NatTrans.app eTruncLTι eTruncGEπ CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Functor.whiskeringRight eTruncGEδLT CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory eTriangleLTGE	—	—
eTriangleLTGE_obj_obj_mor₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.mor₁ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTriangleLTGE CategoryTheory.NatTrans.app eTruncLT CategoryTheory.Functor.id eTruncLTι	—	—
eTriangleLTGE_obj_obj_mor₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.mor₂ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTriangleLTGE CategoryTheory.NatTrans.app CategoryTheory.Functor.id eTruncGE eTruncGEπ	—	—
eTriangleLTGE_obj_obj_mor₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTriangleLTGE CategoryTheory.NatTrans.app eTruncGE CategoryTheory.Functor.comp eTruncLT CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Functor.whiskeringRight eTruncGEδLT	—	—
eTriangleLTGE_obj_obj_obj₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTriangleLTGE eTruncLT	—	—
eTriangleLTGE_obj_obj_obj₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTriangleLTGE	—	—
eTriangleLTGE_obj_obj_obj₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTriangleLTGE eTruncGE	—	—
eTruncGEIsoGEGE_hom 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt eTruncGE CategoryTheory.Functor.comp eTruncGEIsoGEGE eTruncGEToGEGE	—	—
eTruncGEIsoGEGE_hom_inv_id_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncGE CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app eTruncGEπ CategoryTheory.Functor.comp CategoryTheory.Iso.inv eTruncGEIsoGEGE CategoryTheory.CategoryStruct.id	—	eTruncGEToGEGE_app CategoryTheory.Iso.hom_inv_id_app
eTruncGEIsoGEGE_hom_inv_id_app_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncGE CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.id eTruncGEπ CategoryTheory.Functor.comp CategoryTheory.Iso.inv eTruncGEIsoGEGE	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' eTruncGEIsoGEGE_hom_inv_id_app
eTruncGEIsoGEGE_inv_hom_id_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.comp EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncGE CategoryTheory.NatTrans.app CategoryTheory.Iso.inv eTruncGEIsoGEGE CategoryTheory.Functor.map CategoryTheory.Functor.id eTruncGEπ CategoryTheory.CategoryStruct.id	—	eTruncGEToGEGE_app CategoryTheory.Iso.inv_hom_id_app
eTruncGEIsoGEGE_inv_hom_id_app_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncGE CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.inv eTruncGEIsoGEGE CategoryTheory.Functor.map CategoryTheory.Functor.id eTruncGEπ	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' eTruncGEIsoGEGE_inv_hom_id_app
eTruncGEToGEGE_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncGE CategoryTheory.Functor.comp eTruncGEToGEGE CategoryTheory.Functor.map CategoryTheory.Functor.id eTruncGEπ	—	CategoryTheory.Category.id_comp
eTruncGE_obj_bot 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncGE Bot.bot WithBot.bot CategoryTheory.Functor.id	—	—
eTruncGE_obj_coe 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncGE WithBotTop.coe truncGE	—	—
eTruncGE_obj_map_eTruncGEπ_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.map CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncGE CategoryTheory.Functor.id CategoryTheory.NatTrans.app eTruncGEπ	—	truncGE_map_truncGEπ_app CategoryTheory.Limits.HasZeroObject.instFunctor CategoryTheory.zero_map
eTruncGE_obj_map_eTruncGEπ_app_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncGE CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.id eTruncGEπ	—	Mathlib.Tactic.Reassoc.eq_whisker' eTruncGE_obj_map_eTruncGEπ_app
eTruncGE_obj_top 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncGE Top.top WithBot.instTop WithTop.top CategoryTheory.Limits.HasZeroObject.zero' CategoryTheory.Limits.HasZeroObject.instFunctor	—	—
eTruncGEδLT_coe 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.NatTrans.app EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncGE CategoryTheory.Functor.comp eTruncLT CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight CategoryTheory.shiftFunctor Int.instAddMonoid eTruncGEδLT WithBotTop.coe truncGEδLT	—	—
eTruncGEπ_app_eTruncGE_map_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncGE CategoryTheory.NatTrans.app eTruncGEπ CategoryTheory.Functor.map	—	—
eTruncGEπ_app_eTruncGE_map_app_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncGE CategoryTheory.NatTrans.app CategoryTheory.Functor.id eTruncGEπ CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' eTruncGEπ_app_eTruncGE_map_app
eTruncGEπ_bot 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	eTruncGEπ Bot.bot EInt WithBot.bot WithTop CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id	—	—
eTruncGEπ_coe 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	eTruncGEπ WithBotTop.coe truncGEπ	—	—
eTruncGEπ_naturality 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncGE CategoryTheory.NatTrans.app eTruncGEπ CategoryTheory.Functor.map	—	CategoryTheory.NatTrans.naturality
eTruncGEπ_naturality_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncGE CategoryTheory.NatTrans.app CategoryTheory.Functor.id eTruncGEπ CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' eTruncGEπ_naturality
eTruncGEπ_top 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	eTruncGEπ Top.top EInt WithBot.instTop WithTop WithTop.top Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.obj Preorder.smallCategory WithBot.instPreorder WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt eTruncGE CategoryTheory.instZeroHomFunctor	—	—
eTruncLTGEIsoGELT_hom_app_fac 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT eTruncGE CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Functor.map CategoryTheory.NatTrans.app eTruncLTι CategoryTheory.Iso.hom eTruncLTGEIsoGELT	—	CategoryTheory.NatIso.isIso_app_of_isIso instIsIsoFunctorETruncLTGELTSelfToLTGE eTruncLTGELTSelfToLTGE_app CategoryTheory.NatIso.isIso_inv_app CategoryTheory.inv.congr_simp eTruncLTGELTSelfToGELT_app CategoryTheory.IsIso.hom_inv_id_assoc
eTruncLTGEIsoGELT_hom_app_fac' 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.comp EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncGE eTruncLT CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom eTruncLTGEIsoGELT CategoryTheory.Functor.map eTruncLTι	—	CategoryTheory.NatIso.isIso_app_of_isIso instIsIsoFunctorETruncLTGELTSelfToLTGE eTruncLTGELTSelfToLTGE_app CategoryTheory.NatIso.isIso_inv_app CategoryTheory.inv.congr_simp eTruncLTGELTSelfToGELT_app CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality
eTruncLTGEIsoGELT_hom_app_fac'_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT eTruncGE CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.hom eTruncLTGEIsoGELT CategoryTheory.Functor.map CategoryTheory.Functor.id eTruncLTι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' eTruncLTGEIsoGELT_hom_app_fac'
eTruncLTGEIsoGELT_hom_app_fac_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT eTruncGE CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.id eTruncLTι CategoryTheory.Functor.comp CategoryTheory.Iso.hom eTruncLTGEIsoGELT	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' eTruncLTGEIsoGELT_hom_app_fac
eTruncLTGEIsoGELT_hom_naturality 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT eTruncGE CategoryTheory.Functor.comp CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Iso.hom eTruncLTGEIsoGELT	—	CategoryTheory.NatTrans.naturality
eTruncLTGEIsoGELT_hom_naturality_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT eTruncGE CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.hom eTruncLTGEIsoGELT	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' eTruncLTGEIsoGELT_hom_naturality
eTruncLTGEIsoGELT_naturality_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE eTruncGE CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Iso.hom eTruncLTGEIsoGELT	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.NatIso.isIso_app_of_isIso instIsIsoFunctorETruncLTGELTSelfToLTGE eTruncLTGELTSelfToLTGE_app eTruncLTGEIsoGELT_hom_app_fac_assoc CategoryTheory.NatTrans.naturality_assoc CategoryTheory.Functor.map_comp_assoc CategoryTheory.NatTrans.naturality eTruncLT_map_app_eTruncLTι_app CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc eTruncLTGEIsoGELT_hom_app_fac eTruncLT_map_app_eTruncLTι_app_assoc
eTruncLTGEIsoGELT_naturality_app_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE eTruncGE CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Functor.comp CategoryTheory.Iso.hom eTruncLTGEIsoGELT	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' eTruncLTGEIsoGELT_naturality_app
eTruncLTGELTSelfToGELT_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT eTruncGE eTruncLTGELTSelfToGELT CategoryTheory.Functor.id eTruncLTι	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
eTruncLTGELTSelfToLTGE_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT eTruncGE eTruncLTGELTSelfToLTGE CategoryTheory.Functor.map CategoryTheory.Functor.id eTruncLTι	—	CategoryTheory.Category.comp_id
eTruncLTLTIsoLT_hom 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt eTruncLT eTruncLTLTIsoLT eTruncLTLTToLT	—	—
eTruncLTLTIsoLT_hom_inv_id_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Functor.map CategoryTheory.NatTrans.app eTruncLTι CategoryTheory.Iso.inv eTruncLTLTIsoLT CategoryTheory.CategoryStruct.id	—	eTruncLTLTToLT_app CategoryTheory.Iso.hom_inv_id_app
eTruncLTLTIsoLT_hom_inv_id_app_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.id eTruncLTι CategoryTheory.Functor.comp CategoryTheory.Iso.inv eTruncLTLTIsoLT	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' eTruncLTLTIsoLT_hom_inv_id_app
eTruncLTLTIsoLT_inv_hom_id_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.inv eTruncLTLTIsoLT CategoryTheory.Functor.map eTruncLTι CategoryTheory.CategoryStruct.id	—	eTruncLTLTToLT_app CategoryTheory.Iso.inv_hom_id_app
eTruncLTLTIsoLT_inv_hom_id_app_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.inv eTruncLTLTIsoLT CategoryTheory.Functor.map CategoryTheory.Functor.id eTruncLTι	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' eTruncLTLTIsoLT_inv_hom_id_app
eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_obj 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.inv eTruncLTLTIsoLT CategoryTheory.Functor.map eTruncLTι CategoryTheory.CategoryStruct.id	—	eTruncLT_obj_map_eTruncLTι_app eTruncLTLTIsoLT_inv_hom_id_app
eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_obj_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.inv eTruncLTLTIsoLT CategoryTheory.Functor.map CategoryTheory.Functor.id eTruncLTι	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_obj
eTruncLTLTToLT_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT eTruncLTLTToLT CategoryTheory.Functor.map CategoryTheory.Functor.id eTruncLTι	—	CategoryTheory.Category.comp_id
eTruncLT_map_app_eTruncLTι_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Functor.map eTruncLTι	—	—
eTruncLT_map_app_eTruncLTι_app_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Functor.id eTruncLTι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' eTruncLT_map_app_eTruncLTι_app
eTruncLT_map_eq_truncLTι 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.map EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT WithBotTop.coe Top.top WithBotTop WithBot.instTop WithTop.top CategoryTheory.homOfLE truncLTι	—	—
eTruncLT_obj_bot 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT Bot.bot WithBot.bot CategoryTheory.Limits.HasZeroObject.zero' CategoryTheory.Limits.HasZeroObject.instFunctor	—	—
eTruncLT_obj_coe 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT WithBotTop.coe truncLT	—	—
eTruncLT_obj_map_eTruncLTι_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.map CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT CategoryTheory.Functor.id CategoryTheory.NatTrans.app eTruncLTι	—	CategoryTheory.Limits.HasZeroObject.instFunctor CategoryTheory.zero_map truncLT_map_truncLTι_app
eTruncLT_obj_map_eTruncLTι_app_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.id eTruncLTι	—	Mathlib.Tactic.Reassoc.eq_whisker' eTruncLT_obj_map_eTruncLTι_app
eTruncLT_obj_map_eTruncLTι_app_eTruncLT_map_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app eTruncLTι	—	le_top CategoryTheory.Limits.HasZeroObject.instFunctor CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditiveObjEIntFunctorETruncLT CategoryTheory.Limits.zero_comp CategoryTheory.Functor.map_comp CategoryTheory.Limits.comp_zero CategoryTheory.NatTrans.naturality truncLT_map_truncLTι_app CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
eTruncLT_obj_map_eTruncLTι_app_eTruncLT_map_app_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.id eTruncLTι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' eTruncLT_obj_map_eTruncLTι_app_eTruncLT_map_app
eTruncLT_obj_top 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT Top.top WithBot.instTop WithTop.top CategoryTheory.Functor.id	—	—
eTruncLT_ι_bot 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	eTruncLTι Bot.bot EInt WithBot.bot WithTop Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj Preorder.smallCategory WithBot.instPreorder WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt eTruncLT CategoryTheory.Functor.id CategoryTheory.instZeroHomFunctor	—	—
eTruncLT_ι_coe 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	eTruncLTι WithBotTop.coe truncLTι	—	—
eTruncLT_ι_top 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	eTruncLTι Top.top EInt WithBot.instTop WithTop WithTop.top CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj Preorder.smallCategory WithBot.instPreorder WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt eTruncLT	—	—
eTruncLTι_naturality 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app eTruncLTι	—	CategoryTheory.NatTrans.naturality
eTruncLTι_naturality_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.id eTruncLTι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' eTruncLTι_naturality
instAdditiveObjEIntFunctorETruncGE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.Additive CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncGE	—	CategoryTheory.Functor.instAdditiveId instAdditiveTruncGE CategoryTheory.Limits.HasZeroObject.instFunctor CategoryTheory.Functor.instAdditiveOfNat
instAdditiveObjEIntFunctorETruncLT 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.Additive CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT	—	CategoryTheory.Limits.HasZeroObject.instFunctor CategoryTheory.Functor.instAdditiveOfNat instAdditiveTruncLT CategoryTheory.Functor.instAdditiveId
instIsGEObjEIntFunctorETruncGE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncGE	—	instIsGEObjTruncGE_1 isGE_of_isZero CategoryTheory.Limits.HasZeroObject.instFunctor
instIsGEObjEIntFunctorETruncLT 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsGE CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT	—	isGE_of_isZero CategoryTheory.Limits.HasZeroObject.instFunctor instIsGEObjTruncLT
instIsIsoAppETruncLTιObjEIntFunctorETruncLT 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.IsIso CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT CategoryTheory.Functor.id CategoryTheory.NatTrans.app eTruncLTι	—	eTruncLT_obj_map_eTruncLTι_app instIsIsoMapObjEIntFunctorETruncLTAppETruncLTι
instIsIsoFunctorETruncGEπBotEInt 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt eTruncGE Bot.bot WithBot.bot eTruncGEπ	—	CategoryTheory.IsIso.id
instIsIsoFunctorETruncLTGELTSelfToGELT 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt eTruncLT eTruncGE eTruncLTGELTSelfToGELT	—	CategoryTheory.NatTrans.isIso_iff_isIso_app eTruncLTGELTSelfToGELT_app CategoryTheory.Limits.HasZeroObject.instFunctor CategoryTheory.Functor.map_isZero CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditiveObjEIntFunctorETruncGE CategoryTheory.Functor.zero_obj instIsIsoAppTruncLTιObjTruncGETruncLT CategoryTheory.Limits.IsZero.eq_of_src instAdditiveObjEIntFunctorETruncLT
instIsIsoFunctorETruncLTGELTSelfToLTGE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt eTruncLT eTruncGE eTruncLTGELTSelfToLTGE	—	CategoryTheory.NatTrans.isIso_iff_isIso_app CategoryTheory.Limits.HasZeroObject.instFunctor eTruncLTGELTSelfToLTGE_app CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditiveObjEIntFunctorETruncGE CategoryTheory.zero_map instIsIsoMapTruncLTTruncGEAppTruncLTι instAdditiveTruncLT CategoryTheory.Functor.map_isZero CategoryTheory.Functor.zero_obj CategoryTheory.Functor.map_id
instIsIsoFunctorETruncLTιTopEInt 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt eTruncLT Top.top WithBot.instTop WithTop.top CategoryTheory.Functor.id eTruncLTι	—	CategoryTheory.IsIso.id
instIsIsoMapObjEIntFunctorETruncLTAppETruncLTι 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.IsIso CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app eTruncLTι	—	isIso_eTruncLT_obj_map_truncLTπ_app le_refl
instIsLEObjEIntFunctorETruncGE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncGE	—	instIsLEObjTruncGE isLE_of_isZero CategoryTheory.Limits.HasZeroObject.instFunctor
instIsLEObjEIntFunctorETruncLT 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsLE CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT	—	isLE_of_isZero CategoryTheory.Limits.HasZeroObject.instFunctor instIsLEObjTruncLT
isGE_eTruncGE_obj_obj 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid WithBotTop Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt WithBotTop.coe	IsGE CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncGE	—	isGE_of_ge instIsGEObjTruncGE isGE_of_isZero CategoryTheory.Limits.HasZeroObject.instFunctor CategoryTheory.Functor.zero_obj
isIso_eTruncGEIsoGEGE 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt eTruncGE CategoryTheory.Functor.comp eTruncGEToGEGE	—	CategoryTheory.NatTrans.isIso_iff_isIso_app eTruncGEToGEGE_app isIso_eTruncGE_obj_map_truncGEπ_app
isIso_eTruncGE_obj_map_truncGEπ_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	CategoryTheory.IsIso CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncGE CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app eTruncGEπ	—	CategoryTheory.Functor.map_isIso CategoryTheory.NatIso.isIso_app_of_isIso instIsIsoFunctorETruncGEπBotEInt isIso_truncGE_map_truncGEπ_app CategoryTheory.Limits.IsZero.eq_of_src CategoryTheory.Limits.HasZeroObject.instFunctor
isIso_eTruncLTLTIsoLT 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt eTruncLT eTruncLTLTToLT	—	CategoryTheory.NatTrans.isIso_iff_isIso_app eTruncLTLTToLT_app isIso_eTruncLT_obj_map_truncLTπ_app
isIso_eTruncLT_obj_map_truncLTπ_app 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	CategoryTheory.IsIso CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app eTruncLTι	—	CategoryTheory.Limits.IsZero.eq_of_src CategoryTheory.Limits.HasZeroObject.instFunctor isIso_truncLT_map_truncLTι_app CategoryTheory.Functor.map_isIso CategoryTheory.IsIso.id CategoryTheory.NatIso.isIso_app_of_isIso instIsIsoFunctorETruncLTιTopEInt
isLE_eTruncLT_obj_obj 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt WithBotTop.coe	IsLE CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT	—	isLE_of_isZero CategoryTheory.Limits.HasZeroObject.instFunctor isLE_of_le instIsLEObjTruncLTHSubIntOfNat
isZero_eTruncGE_obj_obj 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid WithBotTop Preorder.toLT WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt WithBotTop.coe	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncGE	—	isLE_of_le isZero_truncGE_obj_of_isLE CategoryTheory.Limits.HasZeroObject.instFunctor
isZero_eTruncLT_obj_obj 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt WithBotTop.coe	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor CategoryTheory.Functor.category eTruncLT	—	CategoryTheory.Limits.HasZeroObject.instFunctor isGE_of_ge isZero_truncLT_obj_of_isGE

---

← Back to Index