instHasInitial — Mathlib

English

In the category WithInitial(C) there exists an initial object. Concretely, there is a distinguished object star (the added initial object) such that for every object X in WithInitial(C) there is a unique morphism star → X.

Русский

В категории WithInitial(C) существует начальный объект. Конкретно, фиксировано особый объект star, такой что для каждого объекта X в WithInitial(C) существует единственный морфизм star → X.

LaTeX

$$$$ \text{There exists an initial object in } \mathrm{WithInitial}(\mathcal{C}). $$$$

Lean4

instance : Limits.HasInitial (WithInitial C) :=
  Limits.hasInitial_of_unique star

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