isClosed_zeroLocus

Mathlib.RingTheory.Spectrum.Prime.Topology

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

English

For any subset s of R, zeroLocus s is closed.

Русский

Для любого подмножества s кольца R нулевая локус замкнута.

LaTeX

$$$\\mathrm{IsClosed}\\bigl(\\mathrm{zeroLocus}(s)\\bigr)$$$

Lean4

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

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

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

Разделы

Аффилиация

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