cone

Mathlib.CategoryTheory.Sites.Sheaf

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Presieve.FamilyOfElements.SieveCompatible.cone

Lean4

/-- The cone corresponding to a sieve_compatible family of elements, dot notation enabled. -/
@[simp]
def _root_.CategoryTheory.Presieve.FamilyOfElements.SieveCompatible.cone : Cone (S.arrows.diagram.op ⋙ P)
    where
  pt := E.unop
  π := (conesEquivSieveCompatibleFamily P S E).invFun ⟨x, hx⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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