instCoeHeadObjOppositeToPresheaf

Mathlib.CategoryTheory.Subpresheaf.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subpresheaf.instCoeHeadObjOppositeToPresheaf

Lean4

instance {U} : CoeHead (G.toPresheaf.obj U) (F.obj U) where coe := Subtype.val

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

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

Разделы

Аффилиация

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