Theorem CategoryTheory.Functor.IsCartesian.map_uniq

Modification history

2024-06-18 06:24
Mathlib/CategoryTheory/FiberedCategory/Cartesian.lean
feat(FiberedCategory/Cartesian): define cartesian morphisms (#13393) …
Added CategoryTheory.Functor.IsCartesian.map_uniqView on Github →