Theorem CategoryTheory.Functor.isConnected_iff_of_initial

Modification history

2024-12-20 16:26
Mathlib/CategoryTheory/Limits/IsConnected.lean
feat(CategoryTheory): infer connectedness of comma categories from finality/initiality of the functor (#19889)
Added CategoryTheory.Functor.isConnected_iff_of_initialView on Github →