isSifted

Mathlib.CategoryTheory.Filtered.Final

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsFiltered.isSifted

English

If C is filtered, then C is sifted.

Русский

Если C фильтрована, тогда C является sifted.

LaTeX

$$[IsFiltered C] → IsSifted C$$

Lean4

theorem isSifted [IsFiltered C] : IsSifted C where

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

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

Разделы

Аффилиация

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