instRepresentablyFlatOppositeOpOfRepresentablyCoflat

Mathlib.CategoryTheory.Functor.Flat

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

English

If F is RepresentablyFlat, then F is Final.

Русский

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

LaTeX

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

Lean4

instance [RepresentablyCoflat F] : RepresentablyFlat F.op :=
  (representablyFlat_op_iff F).2 inferInstance

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

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

Разделы

Аффилиация

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