opCoproductIsoProduct_inv_comp_ι

English

The inverse of opCoproductIsoProduct' composed with the i-th opposite injection of c equals the i-th projection of f.

Русский

Обратное к opCoproductIsoProduct' после i-й противоположной инъекции кокона равно i-й проекции f.

LaTeX

$$$(\mathrm{opCoproductIsoProduct}'(hc, hf))^{-1} \circ (c_{\mathrm{inj}}(i))^{\mathrm{op}} = f_{\mathrm{proj}}(i)$$$

Lean4

theorem opCoproductIsoProduct_inv_comp_ι [HasCoproduct Z] (b : α) :
    (opCoproductIsoProduct Z).inv ≫ (Sigma.ι Z b).op = Pi.π (op <| Z ·) b :=
  opCoproductIsoProduct'_inv_comp_inj _ _ b

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