generatedNormal — Mathlib

English

The normal subgroupoid generated by X is the infimum of all normal subgroupoids containing X.

Русский

Нормальная подпгруппоида, порожденная X, является наименьшим нормальным подпогруппоидом, содержaщим X.

LaTeX

$$$\mathrm{generatedNormal}\, X = sInf\{S : Subgroupoid\, C \mid (\forall c,d, X\,c\,d \subseteq S.arrows\,c\,d) \land S.IsNormal\}$$$

Lean4

/-- The normal sugroupoid generated by the set of arrows `X` -/
def generatedNormal : Subgroupoid C :=
  sInf {S : Subgroupoid C | (∀ c d, X c d ⊆ S.arrows c d) ∧ S.IsNormal}

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