instFaithfulPreordCatPreordToCat

Mathlib.Order.Category.Preord

URI: https://scilib.ai/kg/mathlib#instFaithfulPreordCatPreordToCat

English

The forgetful functor from Preord to Cat is faithful.

Русский

Функтор забывания из Preord в Cat является верным ( faithful ).

LaTeX

$$$F:\\text{Preord} \\to \\text{Cat}$ is faithful, i.e., if F(f) = F(g) then f = g.$$

Lean4

instance : preordToCat.{u}.Faithful where map_injective h := by ext x; exact Functor.congr_obj h x

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

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

Разделы

Аффилиация

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