Commit 2023-03-11 14:23 22076520

View on Github →

feat: port CategoryTheory.IsConnected (#2443)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/IsConnected.lean

added theorem CategoryTheory.IsConnected.of_any_functor_const_on_obj

added theorem CategoryTheory.IsConnected.of_constant_of_preserves_morphisms

added theorem CategoryTheory.IsConnected.of_induct

added def CategoryTheory.Zag

added def CategoryTheory.Zigzag.setoid

added def CategoryTheory.Zigzag

added theorem CategoryTheory.any_functor_const_on_obj

added theorem CategoryTheory.constant_of_preserves_morphisms

added def CategoryTheory.discreteIsConnectedEquivPunit

added theorem CategoryTheory.equiv_relation

added theorem CategoryTheory.exists_zigzag'

added theorem CategoryTheory.induct_on_objects

added theorem CategoryTheory.isConnected_of_equivalent

added theorem CategoryTheory.isConnected_of_isConnected_op

added theorem CategoryTheory.isConnected_of_zigzag

added theorem CategoryTheory.isConnected_zigzag

added theorem CategoryTheory.isPreconnected_induction

added theorem CategoryTheory.isPreconnected_of_equivalent

added theorem CategoryTheory.isPreconnected_of_isPreconnected_op

added def CategoryTheory.isoConstant

added theorem CategoryTheory.nat_trans_from_is_connected

added theorem CategoryTheory.zag_of_zag_obj

added theorem CategoryTheory.zag_symmetric

added theorem CategoryTheory.zigzag_equivalence

added theorem CategoryTheory.zigzag_isConnected

added theorem CategoryTheory.zigzag_obj_of_zigzag

added theorem CategoryTheory.zigzag_symmetric