Cover

Mathlib.CategoryTheory.Sites.Grothendieck

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GrothendieckTopology.Cover

Lean4

/-- `J.Cover X` denotes the poset of covers of `X` with respect to the
Grothendieck topology `J`. -/
def Cover (X : C) : Type max u v :=
  { S : Sieve X // S ∈ J X }
deriving Preorder

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

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

Разделы

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

Аффилиация

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