prodZeroIso_iso_inv_snd — Mathlib

English

The inverse of the product-zero isomorphism composed with the first projection gives the identity on X.

Русский

Обратный к изоморфизму X ≅ X × 0, после применения проекции fst возвращает тождественный морфизм на X.

LaTeX

$$$$ (\text{prodZeroIso } X)^{-1} \circ \mathrm{prod.fst} = \mathrm{id}_X. $$$$

Lean4

@[simp]
theorem prodZeroIso_iso_inv_snd (X : C) : (prodZeroIso X).inv ≫ prod.fst = 𝟙 X :=
  by
  dsimp [prodZeroIso, binaryFanZeroRight]
  simp

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