zeroLocus_singleton_zero

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

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

English

For the singleton set {0}, the vanishing locus is the entire space.

Русский

Для множества {0} нулевая локализация равна всей области.

LaTeX

$$$ \operatorname{zeroLocus} 𝒜 ({0} : \mathrm{Set} A) = \mathrm{Set.univ}$$$

Lean4

@[simp]
theorem zeroLocus_singleton_zero : zeroLocus 𝒜 ({0} : Set A) = Set.univ :=
  zeroLocus_bot _

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

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

Разделы

Аффилиация

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