of_isInitial

Mathlib.CategoryTheory.Filtered.Basic

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$\text{IsInitial}(X) \Rightarrow \mathrm{IsCofiltered} C$$$

Lean4

theorem of_isInitial {X : C} (h : IsInitial X) : IsCofiltered C :=
  of_cone_nonempty.{v} _ fun {_} _ _ _ => ⟨⟨X, ⟨fun _ => h.to _, fun _ _ _ => h.hom_ext _ _⟩⟩⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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