THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines a few basic properties of groupoids.
theorem
category_theory.groupoid.is_thin_iff
(C : Type u_1)
[category_theory.groupoid C] :
quiver.is_thin C ↔ ∀ (c : C), subsingleton (c ⟶ c)
def
category_theory.groupoid.is_totally_disconnected
(C : Type u_1)
[category_theory.groupoid C] :
Prop
A subgroupoid is totally disconnected if it only has loops.