faithful_inverse

Mathlib.CategoryTheory.Equivalence

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Equivalence.faithful_inverse

English

The inverse equivalence has a faithful functor as well.

Русский

Обратная эквивалентность тоже имеет верный функтор.

LaTeX

$$$e.inverse.functor\; \text{ is faithful}$$$

Lean4

instance faithful_inverse (e : C ≌ E) : e.inverse.Faithful :=
  e.fullyFaithfulInverse.faithful

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

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

Разделы

Аффилиация

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