instFaithfulUliftFunctor

Mathlib.Topology.Category.TopCat.ULift

URI: https://scilib.ai/kg/mathlib#TopCat.instFaithfulUliftFunctor

English

The ulift functor is faithful (injective on hom-sets).

Русский

Функтор ulift верен (инъективен на множества морфизмов).

LaTeX

$$$\\text{uliftFunctor is faithful}. $$$

Lean4

instance : uliftFunctor.{v, u}.Faithful :=
  uliftFunctorFullyFaithful.faithful

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

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

Разделы

Аффилиация

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