union_zeroLocus — Mathlib

English

The union of zero loci of s and s' equals the zero locus of the intersection of span(s) and span(s'):

Русский

Объединение нулевых локусов s и s' равно нулевому локусу пересечения образов span(s) и span(s'):

LaTeX

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

Lean4

theorem union_zeroLocus (s s' : Set R) :
    zeroLocus s ∪ zeroLocus s' = zeroLocus (Ideal.span s ⊓ Ideal.span s' : Ideal R) :=
  by
  rw [zeroLocus_inf]
  simp

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