instIsFilteredProd

Mathlib.CategoryTheory.Filtered.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instIsFilteredProd

English

If C and D are IsFiltered, then their product is IsFiltered.

Русский

Если C и D фильтрованы, то их произведение C × D фильтровано.

LaTeX

$$$\\mathrm{IsFiltered}(C) \\land \\mathrm{IsFiltered}(D) \\Rightarrow \\mathrm{IsFiltered}(C \\times D)$$$

Lean4

instance [IsFiltered C] [IsFiltered D] : IsFiltered (C × D) where

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

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

Разделы

Аффилиация

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