instIsRepresentableObjOppositeTypeYoneda

Mathlib.CategoryTheory.Yoneda

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.instIsRepresentableObjOppositeTypeYoneda

English

If F is corepresentable by X via a given e, then F is corepresentable.

Русский

Если F корпредставимо по X через данное e, то F корпредставимо.

LaTeX

$$$ F \\text{ IsCorepresentable} $$$

Lean4

instance {X : C} : IsRepresentable (yoneda.obj X) :=
  IsRepresentable.mk' (Iso.refl _)

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

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

Разделы

Аффилиация

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