isOpen_basicOpen

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

URI: https://scilib.ai/kg/mathlib#ProjectiveSpectrum.isOpen_basicOpen

English

The basicOpen sets are open; each basicOpen 𝒜 a is an open subset of the projective spectrum 𝒜.

Русский

Множества basicOpen 𝒜 a являются открытыми подмножествами проективного спектра 𝒜.

LaTeX

$$$\text{IsOpen}(\mathrm{basicOpen}_{\mathcal{A}}(a))$$$

Lean4

theorem isOpen_basicOpen {a : A} : IsOpen (basicOpen 𝒜 a : Set (ProjectiveSpectrum 𝒜)) :=
  (basicOpen 𝒜 a).isOpen

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

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

Разделы

Аффилиация

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