basicOpen_zero

Mathlib.AlgebraicGeometry.Scheme

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

English

The basic open corresponding to the zero section is empty.

Русский

Базовое открытое, соответствующее нулевой секции, равно пустому множеству.

LaTeX

$$$X.basicOpen (0 : \\Gamma(X,U)) = \\varnothing$$$

Lean4

@[simp]
theorem basicOpen_zero (U : X.Opens) : X.basicOpen (0 : Γ(X, U)) = ⊥ :=
  LocallyRingedSpace.basicOpen_zero _ U

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

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

Разделы

Аффилиация

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