inr_biprodXIso_inv — Mathlib

English

For every i, the inr morphism composed with the inverse of biprodXIso equals the i-th component of biprod.inr.

Русский

Для каждого i выполняется равенство: biprod.inr ⋅ (biprodXIso K L i)^{-1} = (biprod.inr)_i.

LaTeX

$$$ (\mathrm{biprod.inr}) \circ (\mathrm{biprodXIso}(K,L,i))^{-1} = (\mathrm{biprod.inr})_i. $$$

Lean4

@[reassoc (attr := simp)]
theorem inr_biprodXIso_inv (i : ι) : biprod.inr ≫ (biprodXIso K L i).inv = (biprod.inr : L ⟶ K ⊞ L).f i := by
  simp [biprodXIso]

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