basicOpen

Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.AffineZariskiSite.basicOpen

← MathLib Explorer

English

The basic open set of a section yields an open subset of X.

Русский

Базовый открытый множитель секции образует открытое множество внутри X.

LaTeX

$$$U.basicOpen f \\le U$$$

Lean4

/-- The basic open set of a section, as an element of `AffineZariskiSite`. -/
def basicOpen (U : X.AffineZariskiSite) (f : Γ(X, U.toOpens)) : X.AffineZariskiSite :=
  ⟨X.basicOpen f, U.2.basicOpen f⟩

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

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

Разделы

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

Аффилиация

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