Theorem CategoryTheory.ObjectProperty.FullSubcategory.map_inclusion

Modification history

2025-07-25 21:58

Mathlib/CategoryTheory/ObjectProperty/FullSubcategory.lean

chore: fix more indentation (#27491) …

Modified CategoryTheory.ObjectProperty.FullSubcategory.map_inclusion View on Github →

2025-04-23 10:36

Mathlib/CategoryTheory/ObjectProperty/FullSubcategory.lean

refactor(CategoryTheory): redefine full subcategories using `ObjectProperty` (#22574) …

Added CategoryTheory.ObjectProperty.FullSubcategory.map_inclusion View on Github →