affineBasicOpen_le

Mathlib.AlgebraicGeometry.AffineScheme

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

← MathLib Explorer

English

The basic open inside an affine open V is contained in V.

Русский

Базовое открытое внутри аффинного открытого V содержится в V.

LaTeX

$$$X.affineBasicOpen f \le V$$$

Lean4

theorem _root_.AlgebraicGeometry.Scheme.affineBasicOpen_le (X : Scheme) {V : X.affineOpens} (f : Γ(X, V.1)) :
    X.affineBasicOpen f ≤ V :=
  X.basicOpen_le f

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

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

Разделы

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

Аффилиация

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