instFaithfulCompObjPost

Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CostructuredArrow.instFaithfulCompObjPost

English

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

Русский

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

LaTeX

$$$ \forall F G S, [G.Faithful] : (\mathrm{post}\ F\ G\ S).\mathrm{Faithful}$. $$

Lean4

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

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

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

Разделы

Аффилиация

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