Commit 2026-03-02 15:01 80a41a6f

View on Github →

feat(CategoryTheory/Triangulated/TStructure): more on truncLT and truncGE (#35362)

Estimated changes

Modified Mathlib/CategoryTheory/Triangulated/TStructure/Basic.lean

Modified Mathlib/CategoryTheory/Triangulated/TStructure/TruncLTGE.lean

added theorem CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctorNatTransOfLE_app_hom₂

added theorem CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctorNatTransOfLE_refl

added theorem CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctorNatTransOfLE_trans

added theorem CategoryTheory.Triangulated.TStructure.from_truncGE_obj_ext

added theorem CategoryTheory.Triangulated.TStructure.isGE_iff_isIso_truncGEπ_app

added theorem CategoryTheory.Triangulated.TStructure.isGE_iff_isZero_truncLT_obj

added theorem CategoryTheory.Triangulated.TStructure.isGE_of_isZero

added theorem CategoryTheory.Triangulated.TStructure.isGE_truncGE_obj

added theorem CategoryTheory.Triangulated.TStructure.isLE_iff_isIso_truncLTι_app

added theorem CategoryTheory.Triangulated.TStructure.isLE_iff_isZero_truncGE_obj

added theorem CategoryTheory.Triangulated.TStructure.isLE_of_isZero

added theorem CategoryTheory.Triangulated.TStructure.isLE_truncLT_obj

added theorem CategoryTheory.Triangulated.TStructure.isZero_truncGE_obj_of_isLE

added theorem CategoryTheory.Triangulated.TStructure.isZero_truncLT_obj_of_isGE

added theorem CategoryTheory.Triangulated.TStructure.liftTruncLT_aux

added theorem CategoryTheory.Triangulated.TStructure.liftTruncLT_ι

added theorem CategoryTheory.Triangulated.TStructure.natTransTriangleLTGEOfLE_refl

added theorem CategoryTheory.Triangulated.TStructure.natTransTriangleLTGEOfLE_trans

added theorem CategoryTheory.Triangulated.TStructure.natTransTruncGEOfLE_refl

added theorem CategoryTheory.Triangulated.TStructure.natTransTruncGEOfLE_refl_app

added theorem CategoryTheory.Triangulated.TStructure.natTransTruncGEOfLE_trans

added theorem CategoryTheory.Triangulated.TStructure.natTransTruncGEOfLE_trans_app

added theorem CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_refl

added theorem CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_refl_app

added theorem CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_trans

added theorem CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_trans_app

added theorem CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_ι

added theorem CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_ι_app

added theorem CategoryTheory.Triangulated.TStructure.to_truncLT_obj_ext

added theorem CategoryTheory.Triangulated.TStructure.truncGE_map_truncGEπ_app

added theorem CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_natTransTruncLTOfLE_app

added theorem CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_truncLTι

added theorem CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_truncLTι_app

added theorem CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE

added theorem CategoryTheory.Triangulated.TStructure.truncGEπ_comp_truncGEδLT

added theorem CategoryTheory.Triangulated.TStructure.truncGEπ_comp_truncGEδLT_app

added theorem CategoryTheory.Triangulated.TStructure.truncGEπ_naturality

added theorem CategoryTheory.Triangulated.TStructure.truncLT_map_truncLTι_app

added theorem CategoryTheory.Triangulated.TStructure.truncLTι_comp_truncGEπ

added theorem CategoryTheory.Triangulated.TStructure.truncLTι_comp_truncGEπ_app

added theorem CategoryTheory.Triangulated.TStructure.π_natTransTruncGEOfLE

added theorem CategoryTheory.Triangulated.TStructure.π_natTransTruncGEOfLE_app