instHasFiniteProductsLocalization'

Mathlib.CategoryTheory.Localization.FiniteProducts

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Localization.instHasFiniteProductsLocalization'

English

Assuming a HasLocalization, the localization with Q' has finite products.

Русский

При наличии локализации HasLocalization локализация с Q' имеет конечные произведения.

LaTeX

$$$ [W.HasLocalization] : HasFiniteProducts W.Localization' $$$

Lean4

instance [W.HasLocalization] : HasFiniteProducts (W.Localization') :=
  hasFiniteProducts W.Q' W

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru