instFaithfulWitness

Mathlib.CategoryTheory.UnivLE

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

English

There is a faithful witness for UnivLE, namely the functor F ↦ F on morphisms is faithful.

Русский

Существуют достоверные свидетели UnivLE, например, отображение на отображения через Functor Faithful.

LaTeX

$$$ \\text{UnivLE.witness.Faithful} $$$

Lean4

instance [UnivLE.{max u v, v}] : UnivLE.witness.{u, v}.Faithful :=
  inferInstanceAs <| Functor.Faithful (_ ⋙ _)

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

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

Разделы

Аффилиация

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