inv_prodComparison_map_snd — Mathlib

English

If prodComparison F A B is an isomorphism, then inv(prodComparison F A B) ≫ F.map (snd _ _) = snd _ _.

Русский

Если prodComparison F A B — изоморфизм, то inv(prodComparison F A B) ≫ F.map (snd _ _) = snd _ _.

LaTeX

$$inv (prodComparison F A B) ≫ F.map (snd A B) = snd (F.obj A) (F.obj B)$$

Lean4

@[reassoc (attr := simp)]
theorem inv_prodComparison_map_snd [IsIso (prodComparison F A B)] :
    inv (prodComparison F A B) ≫ F.map (snd _ _) = snd _ _ := by simp [IsIso.inv_comp_eq]

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