presieveOfCovering

Mathlib.Topology.Sheaves.SheafCondition.Sites

URI: https://scilib.ai/kg/mathlib#TopCat.Presheaf.presieveOfCovering

← MathLib Explorer

English

The sieve generated by presieveOfCovering U belongs to Opens.grothendieckTopology on iSup U.

Русский

Сито, порождаваемое presieveOfCovering U, принадлежит Opens.grothendieckTopology на iSup U.

LaTeX

$$mem_grothendieckTopology$$

Lean4

/-- Take `Y` to be `iSup U` and obtain a presieve over `iSup U`. -/
def presieveOfCovering {ι : Type v} (U : ι → Opens X) : Presieve (iSup U) :=
  presieveOfCoveringAux U (iSup U)

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

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

Разделы

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

Аффилиация

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