hasProductsOfShape — Mathlib

English

If C has products of shape J and J is finite, and W is stable under those shape products and contains identities, then D also has products of shape J.

Русский

Пусть C имеет произведения формы J, где J является конечным. Пусть W сохраняет такие произведения и содержит тождества. Тогда и у D есть произведения формы J.

LaTeX

$$$ \\mathrm{HasProductsOfShape}\ J\ C \\Rightarrow \\mathrm{HasProductsOfShape}\ J\ D $$$

Lean4

theorem hasProductsOfShape (J : Type) [Finite J] [HasProductsOfShape J C] [W.IsStableUnderProductsOfShape J] :
    HasProductsOfShape J D :=
  hasLimitsOfShape_iff_isLeftAdjoint_const.2 (HasProductsOfShapeAux.adj L W J).isLeftAdjoint

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