zeroLocus_union — Mathlib

English

Let s and s' be subsets of R. Then the zero locus of their union equals the intersection of their zero loci:

Русский

Пусть S и S' — подмножества кольца R. Тогда нулевой локус объединения равен пересечению нулевых локусов:

LaTeX

$$$\\mathrm{zeroLocus}(s \\cup s') = \\mathrm{zeroLocus}(s) \\cap \\mathrm{zeroLocus}(s').$$$

Lean4

theorem zeroLocus_union (s s' : Set R) : zeroLocus (s ∪ s') = zeroLocus s ∩ zeroLocus s' :=
  (gc_set R).l_sup

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