instIsIsoMapBifunctorMapMap — Mathlib

English

If f and g are isomorphisms, then mapBifunctorMapMap F p f g is an isomorphism.

Русский

Если есть изоморфизмы f и g, то mapBifunctorMapMap F p f g также является изоморфизмом.

LaTeX

$$$IsIso\,(mapBifunctorMapMap F p f g)$ given $IsIso f$ and $IsIso g$$$

Lean4

instance (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) [IsIso f] [IsIso g] : IsIso (mapBifunctorMapMap F p f g) :=
  (inferInstance : IsIso (mapBifunctorMapMapIso F p (asIso f) (asIso g)).hom)

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