mulIsInitial_inv — Mathlib

English

Let I be initial. Then the inverse of the isomorphism mulIsInitial X hI is the canonical map I → prod(X, I).

Русский

Пусть I начальный. Тогда обратный образ изоморфизма mulIsInitial X hI равен каноническому морфизму I → prod(X, I).

LaTeX

$$$(\\mathrm{mulIsInitial} X \\; hI)^{-1} = hI.\\mathrm{to}_{\\mathrm{prod}(X,I)}$$$

Lean4

@[simp]
theorem mulIsInitial_inv (X : C) [HasBinaryProduct X I] (hI : IsInitial I) : (mulIsInitial X hI).inv = hI.to _ :=
  hI.hom_ext _ _

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