initial_of_representablyCoflat

Mathlib.CategoryTheory.Functor.Flat

URI: https://scilib.ai/kg/mathlib#CategoryTheory.initial_of_representablyCoflat

English

If F is RepresentablyCoflat, then F has an initial structure (initial object in the relevant category).

Русский

Если FRepresentablyCoflat, то F обладает начальностью в соответствующей категории.

LaTeX

$$F.Initial$$

Lean4

theorem initial_of_representablyCoflat [h : RepresentablyCoflat F] : F.Initial where out _ := IsFiltered.isConnected _

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

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

Разделы

Аффилиация

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