openCover

Mathlib.AlgebraicGeometry.Cover.Open

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.AffineOpenCover.openCover

Lean4

/-- The open cover associated to an affine open cover. -/
@[simps! I₀ X f]
def openCover {X : Scheme.{u}} (𝒰 : X.AffineOpenCover) : X.OpenCover :=
  AffineCover.cover 𝒰

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

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

Разделы

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

Аффилиация

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