map₂_hom_inv_isIso — Mathlib

English

If η is an isomorphism, then F.map₂ η.hom and F.map₂ η.inv form an isomorphism with the inverse given by the other component.

Русский

Если η — изоморфизм, то F.map₂ η.hom и F.map₂ η.inv образуют изоморфизм, чьим обратным компонентом служит другая часть.

LaTeX

$$IsIso (F.map₂ η.hom)$$

Lean4

@[reassoc]
theorem map₂_hom_inv_isIso {f g : a ⟶ b} (η : f ⟶ g) [IsIso η] : F.map₂ η ≫ F.map₂ (inv η) = 𝟙 (F.map f) := by simp

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