Commit 2024-12-20 16:26 e234a9fb

View on Github →

feat(CategoryTheory): infer connectedness of comma categories from finality/initiality of the functor (#19889)

Estimated changes

Modified Mathlib/CategoryTheory/Comma/Final.lean

Modified Mathlib/CategoryTheory/IsConnected.lean

added theorem CategoryTheory.isConnected_op_iff_isConnected

Modified Mathlib/CategoryTheory/Limits/IsConnected.lean

added theorem CategoryTheory.Functor.isConnected_iff_of_final

added theorem CategoryTheory.Functor.isConnected_iff_of_initial

deleted theorem CategoryTheory.Limits.Types.isConnected_iff_of_final