Commit 2024-02-19 16:57 9ece7063

View on Github →

chore: generalize theorems from IsConnected to IsPreconnected (#10713)

Estimated changes

Modified Mathlib/CategoryTheory/IsConnected.lean

added theorem CategoryTheory.IsPreconnected.of_any_functor_const_on_obj

added theorem CategoryTheory.IsPreconnected.of_constant_of_preserves_morphisms

modified theorem CategoryTheory.equiv_relation

deleted theorem CategoryTheory.isConnected_zigzag

added theorem CategoryTheory.isPreconnected_of_zigzag

added theorem CategoryTheory.isPreconnected_zigzag

added theorem CategoryTheory.nonempty_hom_of_preconnected_groupoid

modified theorem CategoryTheory.zigzag_isConnected

added theorem CategoryTheory.zigzag_isPreconnected

Modified Mathlib/GroupTheory/FreeGroup/NielsenSchreier.lean