Theorem CategoryTheory.Functor.IsStronglyCartesian.isIso_of_base_isIso

Modification history

2024-07-19 09:35
Mathlib/CategoryTheory/FiberedCategory/Cartesian.lean
feat(FiberedCategory/Cartesian): define strongly cartesian morphisms (#13410) …
Added CategoryTheory.Functor.IsStronglyCartesian.isIso_of_base_isIsoView on Github →