instFaithfulElementsπ

Mathlib.CategoryTheory.Elements

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CategoryOfElements.instFaithfulElementsπ

English

The projection π from CategoryOfElements is a faithful functor.

Русский

Проекция π из CategoryOfElements обеспечивает верность (faithfulness).

LaTeX

$$$\\forall {C} [\\mathbf{Category} C], (\\pi F).\\text{Faithful}$$$

Lean4

instance : (π F).Faithful where

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

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

Разделы

Аффилиация

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