final_of_representablyFlat

Mathlib.CategoryTheory.Functor.Flat

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

English

If F is RepresentablyFlat, then F is Final.

Русский

Если F RepresentablyFlat, то F Final.

LaTeX

$$$$ \\mathrm{Final}(F). $$$$

Lean4

theorem final_of_representablyFlat [h : RepresentablyFlat F] : F.Final where out _ := IsCofiltered.isConnected _

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

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

Разделы

Аффилиация

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