Def CategoryTheory.Grothendieck.ιCompMap

Modification history

2025-02-15 12:38

Mathlib/CategoryTheory/Grothendieck.lean

feat(CategoryTheory): `Grothendieck.map` preserves finality (#19073)

Added CategoryTheory.Grothendieck.ιCompMap View on Github →