mk₀

Mathlib.CategoryTheory.ComposableArrows

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ComposableArrows.mk₀

English

Constructor for ComposableArrows C 0, sending an object X ∈ C to the zero-arity ComposableArrows object in C.

Русский

Конструктор для ComposableArrows C 0, отправляющий объект X ∈ C в нуль-арность объекта ComposableArrows.

LaTeX

$$$mk₀ : C \to ComposableArrows C 0$$$

Lean4

/-- Constructor for `ComposableArrows C 0`. -/
@[simps!]
def mk₀ (X : C) : ComposableArrows C 0 :=
  (Functor.const (Fin 1)).obj X

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru