isIso_prod — Mathlib

English

If f: W → Y and g: X → Z are isomorphisms, then the map prod.map f g: W × X → Y × Z is an isomorphism.

Русский

Пусть f: W → Y и g: X → Z – изоморфизмы, тогда prod.map f g: W × X → Y × Z является изоморфизмом.

LaTeX

$$$IsIso(f) \\land IsIso(g) \\Rightarrow IsIso( prod.map f g )$$$

Lean4

instance isIso_prod {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) [IsIso f]
    [IsIso g] : IsIso (prod.map f g) :=
  (prod.mapIso (asIso f) (asIso g)).isIso_hom

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