generated — Mathlib

English

The subgroupoid generated by a family of arrows X is the smallest subgroupoid containing all arrows X; formally, it is the infimum of all subgroupoids that contain X.

Русский

Подгруппойд, порожденный множеством рёбер X, является наименьшим подгруппоидом, содержащим все рёбра из X.

LaTeX

$$$\mathrm{generated}\, X = sInf\{S : Subgroupoid\, C \mid \forall c,d, X\,c\,d \subseteq S.arrows\, c\, d\}$$$

Lean4

/-- The subgroupoid generated by the set of arrows `X` -/
def generated : Subgroupoid C :=
  sInf {S : Subgroupoid C | ∀ c d, X c d ⊆ S.arrows c d}

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