basicOpen_mul

Mathlib.AlgebraicGeometry.Scheme

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

English

The basic open of a product of two sections is the intersection of their basic opens.

Русский

Базовое открытое произведения двух секций равно пересечению их базовых открытых.

LaTeX

$$$X.basicOpen (f g) = X.basicOpen f \\cap X.basicOpen g$$$

Lean4

@[simp]
theorem basicOpen_mul : X.basicOpen (f * g) = X.basicOpen f ⊓ X.basicOpen g :=
  RingedSpace.basicOpen_mul _ _ _

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

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

Разделы

Аффилиация

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