Theorem CategoryTheory.isConnected_op_iff_isConnected

Modification history

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