instHasFiniteProductsLocalization

English

Under the hypotheses, the localization has finite products: for any W, HasFiniteProducts for W.Localization holds.

Русский

При данных предположениях у локализации есть конечные произведения: для любого W выполняется HasFiniteProducts у W.Localization.

LaTeX

$$$ \\mathrm{HasFiniteProducts} (W.Localization) $$$

Lean4

instance : HasFiniteProducts (W.Localization) :=
  hasFiniteProducts W.Q W

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