zeroLocus_empty

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

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

English

The zero locus of the empty set is the entire projective spectrum.

Русский

Нулевая зона пустого множества равна всему проектному спектру.

LaTeX

$$$$ \\mathrm{zeroLocus}(\\mathcal{A}, \\emptyset) = \\mathrm{Set.univ} $$$$

Lean4

@[simp]
theorem zeroLocus_empty : zeroLocus 𝒜 (∅ : Set A) = Set.univ :=
  (gc_set 𝒜).l_bot

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

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

Разделы

Аффилиация

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