binaryProductIso_inv_comp_snd_apply

English

For a given a and z, the second projection of the inverse binary product iso app applied to z equals z.2.

Русский

Для данного a и z вторая проекция обратного двоичного произведения, применённая к z, равна z.2.

LaTeX

$$$ (\mathrm{prod.snd}\ (X := F)).app a ((binaryProductIso F G).inv.app a z) = z.2 $$$

Lean4

@[simp]
theorem binaryProductIso_inv_comp_snd_apply (a : C) (z : (prod F G).obj a) :
    (Limits.prod.snd (X := F)).app a ((binaryProductIso F G).inv.app a z) = z.2 :=
  congr_fun (congr_app (binaryProductIso_inv_comp_snd F G) a) z

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