to_comp — Mathlib

English

Let X be initial in C. For any morphism f: Y → Z, the composites t.to Y ≫ f and t.to Z are equal; i.e., the canonical arrow from the initial object respects composition.

Русский

Пусть X — начальный объект в C. Для любого морфизма f: Y → Z композитныt t.to Y с f и t.to Z равны; то есть каноническое отображение из начального объекта сохраняет композицию.

LaTeX

$$$t : \\text{IsInitial}(X) \\Rightarrow \\forall Y,Z, f:Y\\to Z,\\ t.to Y \\;≫\\; f = t.to Z$$$

Lean4

@[simp]
theorem to_comp {X : C} (t : IsInitial X) {Y Z : C} (f : Y ⟶ Z) : t.to Y ≫ f = t.to Z :=
  t.hom_ext _ _

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