Theorem CategoryTheory.ObjectProperty.HasInducedTStructure.mk'

Modification history

2026-03-03 17:12
Mathlib/CategoryTheory/Triangulated/TStructure/Induced.lean
feat(CategoryTheory/Triangulated/TStucture): induced t-structures (#35367) …
Added CategoryTheory.ObjectProperty.HasInducedTStructure.mk'View on Github →