of_hasInitial

Mathlib.CategoryTheory.Filtered.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsCofiltered.of_hasInitial

English

If C has an initial object, then C is cofiltered.

Русский

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

LaTeX

$$[HasInitial C] ⇒ IsCofiltered C$$

Lean4

instance (priority := 100) of_hasInitial [HasInitial C] : IsCofiltered C :=
  of_isInitial _ initialIsInitial

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

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

Разделы

Аффилиация

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