inl_biprodXIso_inv — Mathlib

English

For every i, the relation between the inl morphism and the inverse of the degree i component of the biprodXIso matches the i-th component of biprod.inl.

Русский

Пусть для каждого i выполняется равенство, связывающее инл-морфизм и обратный компонент изоморфизма biprodXIso на i-ом уровне: biprod.inl ⋅ (biprodXIso K L i)^{-1} = (biprod.inl)_i.

LaTeX

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

Lean4

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

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