Commit 2026-03-03 17:12 6a273184

feat(CategoryTheory/Triangulated/TStucture): induced t-structures (#35367) This PR introduces a typeclass P.HasInducedTStructure t when P is a triangulated subcategory of a (pre)triangulated category C and t a t-structure on C. This essentially says that P is stable by the truncations. In this situation, we define the induced t-structure on the full subcategory defined by P. In particular, this applies to bounded above/bounded below/bounded objects for a given t-structure.