instFaithfulOverToOver

Mathlib.CategoryTheory.Comma.Over.Basic

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

English

Instantiating faithfulness: For any X and F: T ⥤ D with F faithful, (toOver F X) is faithful.

Русский

Для любого X и F: T ⥤ D с F верным, (toOver F X) верно.

LaTeX

$$$\\operatorname{Faithful}(F) \\Rightarrow \\operatorname{Faithful}(\\mathrm{toOver}(F,X))$$$

Lean4

instance (F : D ⥤ T) (X : T) [F.Faithful] : (toOver F X).Faithful :=
  show (CostructuredArrow.pre _ _ _).Faithful from inferInstance

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

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

Разделы

Аффилиация

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