to_comp

Mathlib.CategoryTheory.Limits.Shapes.Terminal

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.initial.to_comp

English

For any f: P → Q, initial.to P ≫ f = initial.to Q.

Русский

Для любой стрелки f: P → Q выполнено initial.to P ≫ f = initial.to Q.

LaTeX

$$$\\forall f:\\, P \\to Q,\\; \\mathrm{initial.to}(P) \\circ f = \\mathrm{initial.to}(Q).$$$

Lean4

@[simp, reassoc]
theorem to_comp [HasInitial C] {P Q : C} (f : P ⟶ Q) : initial.to P ≫ f = initial.to Q := by
  simp [eq_iff_true_of_subsingleton]

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

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

Разделы

Аффилиация

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