faithful

Mathlib.CategoryTheory.Widesubcategory

URI: https://scilib.ai/kg/mathlib#CategoryTheory.wideSubcategory.faithful

← MathLib Explorer

English

The inclusion of a wide subcategory is faithful.

Русский

Включение широкой подкатегории сохраняет монотонность отображения (faithful).

LaTeX

$$$\\text{wideSubcategoryInclusion } P\\; \\text{is faithful}$$$

Lean4

/-- The inclusion of a wide subcategory is faithful. -/
instance faithful : (wideSubcategoryInclusion P).Faithful :=
  inferInstanceAs (wideInducedFunctor WideSubcategory.obj P).Faithful

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

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

Разделы

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

Аффилиация

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