of_hasTerminal

Mathlib.CategoryTheory.Filtered.Basic

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

English

If C has a terminal object, then C is filtered.

Русский

Если в C существует терминальный объект, то C является фильтрованной.

LaTeX

$$$[\\text{HasTerminal}(C)] \\\\Rightarrow \\\\operatorname{IsFiltered}(C).$$$

Lean4

instance (priority := 100) of_hasTerminal [HasTerminal C] : IsFiltered C :=
  of_isTerminal _ terminalIsTerminal

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

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

Разделы

Аффилиация

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