closure_singleton

Mathlib.RingTheory.Spectrum.Prime.Topology

URI: https://scilib.ai/kg/mathlib#PrimeSpectrum.closure_singleton

← MathLib Explorer

English

The closure of a singleton {x} is the zero locus of the ideal x.asIdeal.

Русский

Замыкание множества {x} равно нулевой локусу идеала x.asIdeal.

LaTeX

$$$\\mathrm{closure}({\\{x\\}}) = \\mathrm{zeroLocus}(x.asIdeal)$$$

Lean4

theorem closure_singleton (x) : closure ({ x } : Set (PrimeSpectrum R)) = zeroLocus x.asIdeal := by
  rw [← zeroLocus_vanishingIdeal_eq_closure, vanishingIdeal_singleton]

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

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

Разделы

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

Аффилиация

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