prodEquiv — Mathlib

English

There is a concrete version of prodEquiv: ToType of the product X1 × X2 is equivalent to the pair of ToType objects, under preservations.

Русский

Существуют конкретные версии prodEquiv: ToType произведения X1 × X2 эквивалентна паре ToType(X1), ToType(X2) при сохранении.

LaTeX

$$$ ToType( X_1 \\times X_2 ) \\simeq ToType X_1 \\times ToType X_2 $$$

Lean4

/-- The equivalence `ToType (X₁ ⨯ X₂) ≃ (ToType X₁) × (ToType X₂)`
if `X₁` and `X₂` are objects in a concrete category `C`. -/
noncomputable def prodEquiv : ToType (X₁ ⨯ X₂) ≃ ToType X₁ × ToType X₂ :=
  (PreservesLimitPair.iso (forget C) X₁ X₂ ≪≫ Types.binaryProductIso _ _).toEquiv

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