toZeroHypercover

Mathlib.CategoryTheory.Sites.Hypercover.One

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

Lean4

/-- Forget the `1`-components of a `OneHypercover`. -/
@[simps toPreZeroHypercover]
def toZeroHypercover (E : OneHypercover.{w} J S) : J.toPrecoverage.ZeroHypercover S
    where
  __ := E.toPreZeroHypercover
  mem₀ := E.mem₀

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

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

Разделы

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

Аффилиация

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