instFaithfulCompPreRight

Mathlib.CategoryTheory.Comma.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Comma.instFaithfulCompPreRight

English

If F is faithful, then preRight L F R is faithful.

Русский

Если F верен, тогда preRight L F R сохраняет верность (faithful).

LaTeX

$$$F \text{ Faithful} \Rightarrow (\text{preRight } L F R) \text{ Faithful}.$$$

Lean4

instance (L : A ⥤ T) (F : C ⥤ B) (R : B ⥤ T) [F.Faithful] : (preRight L F R).Faithful :=
  Functor.Faithful.of_iso (preRightIso L F R).symm

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

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

Разделы

Аффилиация

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