initialMul_inv — Mathlib

English

The inverse of the initialMul X is the canonical map from the initial object to the product (initial, X).

Русский

Обратный образ initialMul X — канонический морфизм из начального объекта в произведение (initial, X).

LaTeX

$$$(\\mathrm{initialMul} X)^{-1} = \\mathrm{initial.to} (\\mathrm{prod}(\\initial, X))$$$

Lean4

@[simp]
theorem initialMul_inv (X : C) [HasBinaryProduct (⊥_ C) X] : (initialMul X).inv = initial.to _ :=
  Subsingleton.elim _ _

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