instFullCompPre

Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.StructuredArrow.instFullCompPre

English

If F is full, then (pre S F G) is full.

Русский

Если F полноc, то (pre S F G) полноc.

LaTeX

$$$\text{If } F\text{ is full, then } (\mathrm{pre}\ S\ F\ G).Full$$$

Lean4

instance (S : D) (F : B ⥤ C) (G : C ⥤ D) [F.Full] : (pre S F G).Full :=
  show (Comma.preRight _ _ _).Full from inferInstance

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

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

Разделы

Аффилиация

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