limitMonoid — Mathlib

English

The limit of a diagram into MonCat carries a natural Monoid structure on its carrier.

Русский

Предел диаграммы в MonCat естественным образом несет моноидальную структуру на носителе предельного объекта.

LaTeX

$$$\text{limitMonoid}(F) : Monoid(\text{Types.Small.limitCone}(F \circ \mathrm{forget MonCat}))$$$

Lean4

@[to_additive]
noncomputable instance limitMonoid : Monoid (Types.Small.limitCone.{v, u} (F ⋙ forget MonCat.{u})).pt :=
  inferInstanceAs <| Monoid (Shrink (F ⋙ forget MonCat.{u}).sections)

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