biprodXIso_hom_fst — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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