productEquiv — Mathlib

English

There is an equivalence ToType of the product ∏ᶜ F with the product of the underlying types, i.e. ToType(∏ᶜ F) ≃ ∀ j, ToType(F j).

Русский

Существует эквивалентность типов между ToType(∏ᶜ F) и произведением типов ToType(F j); то есть ToType(∏ᶜ F) ≃ ∀ j, ToType(F j).

LaTeX

$$$ \\text{productEquiv } F : ToType(\\prod^\\mathsf{c} F) \\simeq \\forall j, ToType(F j) $$$

Lean4

/-- The equivalence `ToType (∏ᶜ F) ≃ ∀ j, ToType (F j)` if `F : J → C` is a family of objects
in a concrete category `C`. -/
noncomputable def productEquiv : ToType (∏ᶜ F) ≃ ∀ j, ToType (F j) :=
  ((PreservesProduct.iso (forget C) F) ≪≫ (Types.productIso.{w, v} fun j => ToType (F j))).toEquiv

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