prod — Mathlib

English

There is a natural isomorphism from F.prod' G followed by snd to G, i.e. (F.prod' G) ⋅ snd ≅ G.

Русский

Существует естественное изоморфизмe из F.prod' G, затем snd, в G.

LaTeX

$$$(F.prod' G) \\cdot \\mathrm{snd} \\cong G$$$

Lean4

/-- The Cartesian product of two equivalences of categories. -/
@[simps]
def prod (E₁ : A ≌ B) (E₂ : C ≌ D) : A × C ≌ B × D
    where
  functor := E₁.functor.prod E₂.functor
  inverse := E₁.inverse.prod E₂.inverse
  unitIso := NatIso.prod E₁.unitIso E₂.unitIso
  counitIso := NatIso.prod E₁.counitIso E₂.counitIso

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