of_comp

Mathlib.CategoryTheory.Functor.FullyFaithful

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.Faithful.of_comp

← MathLib Explorer

English

If the composition F ⋙ G is faithful, then F is faithful.

Русский

Если состав F ⋙ G верен, то F верен.

LaTeX

$$$[ (F \circ G)\text{ Faithful}] \Rightarrow F\text{ Faithful}$$$

Lean4

theorem of_comp [(F ⋙ G).Faithful] : F.Faithful :=
  -- Porting note: (F ⋙ G).map_injective.of_comp has the incorrect type

  { map_injective := fun {_ _} => Function.Injective.of_comp (F ⋙ G).map_injective }

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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