isCorepresentable

Mathlib.CategoryTheory.Yoneda

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

English

If F is corepresentable by X, then F is corepresentable.

Русский

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

LaTeX

$$$ F.\\IsCorepresentable $$$

Lean4

theorem isCorepresentable {F : C ⥤ Type v} {X : C} (e : F.CorepresentableBy X) : F.IsCorepresentable where
  has_corepresentation := ⟨X, ⟨e⟩⟩

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

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

Разделы

Аффилиация

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