instHasProduct

Mathlib.Order.Category.OmegaCompletePartialOrder

URI: https://scilib.ai/kg/mathlib#ωCPO.HasProducts.instHasProduct

English

For any index set J and any family f: J → ωCPO, the product exists.

Русский

Для любой индексной множества J и любой семейства объектов f: J → ωCPO существует произведение.

LaTeX

$$$\forall J\;\forall f: J \to ωCPO:\; \text{HasProduct}(f).$$$

Lean4

instance (J : Type v) (f : J → ωCPO.{v}) : HasProduct f :=
  HasLimit.mk ⟨_, isProduct _ f⟩

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

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

Разделы

Аффилиация

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