isClosed_zeroLocus

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

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

English

For any subset s of A, the zero locus is a closed set in the Zariski topology.

Русский

Для любого подмножества s ⊆ A нуль-множество является замкнутым множеством в Zariski топологии.

LaTeX

$$$ \text{IsClosed}(\operatorname{zeroLocus}_{\mathcal{A}}(s)) $$$

Lean4

theorem isClosed_zeroLocus (s : Set A) : IsClosed (zeroLocus 𝒜 s) :=
  by
  rw [isClosed_iff_zeroLocus]
  exact ⟨s, rfl⟩

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

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

Разделы

Аффилиация

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