mulInitial_inv — Mathlib

English

The inverse of mulInitial X is the canonical map from the initial object to the product ⊥ × X.

Русский

Обратный образ mulInitial X есть канонический морфизм из начального объекта в произведение ⊥ × X.

LaTeX

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

Lean4

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

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