instFaithfulObjCompPost

Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

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

English

If F is faithful, then (post S F G) is faithful.

Русский

Если F вернообразна, то (post S F G) вернообразна.

LaTeX

$$$\text{If } F\text{ is faithful, then } (\mathrm{post}\ S\ F\ G).Faithful$$$

Lean4

instance (S : C) (F : B ⥤ C) (G : C ⥤ D) : (post S F G).Faithful where
  map_injective {_ _} _ _ h := by simpa [ext_iff] using h

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

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

Разделы

Аффилиация

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