affineOpens

Mathlib.AlgebraicGeometry.AffineScheme

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

English

The affineOpens X is the set of affine opens inside X.

Русский

Множество affineOpens X состоит из аффинных открытых подмножеств X.

LaTeX

$$$$ \text{affineOpens}(X) = \{ U \in X.\mathrm{Opens} \mid \mathrm{IsAffineOpen}(U) \}. $$$$

Lean4

/-- The set of affine opens as a subset of `opens X`. -/
def affineOpens (X : Scheme) : Set X.Opens :=
  {U : X.Opens | IsAffineOpen U}

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

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

Разделы

Аффилиация

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