biprodXIso_hom_snd — Mathlib

English

For every i, the isomorphism component hom followed by biprod.snd equals the i-th component of biprod.snd.

Русский

Для каждого i имеет место равенство: (biprodXIso K L i).hom ⋅ biprod.snd = biprod.snd_i.

LaTeX

$$$ (\mathrm{biprodXIso}(K,L,i))_{\mathrm{hom}} \circ \mathrm{biprod.snd}_i = \mathrm{biprod.snd}.f i. $$$

Lean4

@[reassoc (attr := simp)]
theorem biprodXIso_hom_snd (i : ι) : (biprodXIso K L i).hom ≫ biprod.snd = (biprod.snd : K ⊞ L ⟶ L).f i := by
  simp [biprodXIso]

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