instFaithfulIncl

Mathlib.CategoryTheory.FintypeCat

URI: https://scilib.ai/kg/mathlib#FintypeCat.Skeleton.instFaithfulIncl

English

The inclusion functor from FintypeCat.Skeleton to FintypeCat is faithful.

Русский

Включение FintypeCat.Skeleton в FintypeCat является верным (фиделным).

LaTeX

$$$\\text{incl} : \\text{FintypeCat.Skeleton} \\to \\text{FintypeCat}$ is faithful$$

Lean4

instance : incl.Faithful where

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

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

Разделы

Аффилиация

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