isThin_iff — Mathlib

English

For any Subgroupoid S of a groupoid C, S is thin if and only if every endomorphism set S.arrows c c is a singleton (i.e., has at most one element) for every object c of S.

Русский

Для подгруппоида S внутри группоида C: S тонок тогда и только тогда, когда множества концевых стрелок S.arrows c c состоят ровно из одного элемента (для каждого объекта c из S).

LaTeX

$$$S.IsThin \\iff \\forall c : S.objs, Subsingleton\\ (S.arrows\\ c\\ c)$$$

Lean4

nonrec theorem isThin_iff : S.IsThin ↔ ∀ c : S.objs, Subsingleton (S.arrows c c) :=
  isThin_iff _

Похожие утверждения