instIsFilteredOrEmpty

Mathlib.CategoryTheory.Filtered.Small

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

English

The SmallFilteredIntermediate F is IsFilteredOrEmpty.

Русский

Маленькая фильтрованная промежуточная категория F является либо фильтрованной, либо пустой.

LaTeX

$$$\\operatorname{IsFilteredOrEmpty}(\\mathrm{SmallFilteredIntermediate}(F))$$$

Lean4

instance : IsFilteredOrEmpty (SmallFilteredIntermediate F) :=
  IsFilteredOrEmpty.of_equivalence (equivSmallModel _)

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

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

Разделы

Аффилиация

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