mathlib3

f187f107 - feat(category_theory/groupoid/*): `is_thin` and `is_totally_disconnected` (#17122)

feat(category_theory/groupoid/*): `is_thin` and `is_totally_disconnected` (#17122) Define `is_thin` for quivers and subgroupoids and `is_totally_disconnected` for groupoids and subgroupoids. Co-authored-by: Junyan Xu <junyanxumath@gmail.com>