Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-06 21:31 7ec4fcc3

View on Github →

feat(category_theory): connected components of a category (#5425)

Estimated changes

Created src/category_theory/connected_components.lean

added def category_theory.component.ι

added def category_theory.component

added def category_theory.connected_components

added def category_theory.decomposed

added def category_theory.decomposed_equiv

added def category_theory.decomposed_to

added def category_theory.inclusion

added theorem category_theory.inclusion_comp_decomposed_to