zeroLocus_inf — Mathlib

English

For ideals I and J in R, the zero locus of their intersection equals the union of their zero loci:

Русский

Для идеалов I и J в R нулевой локус пересечения равен объединению нулевых локусов:

LaTeX

$$$\\mathrm{zeroLocus}(I \\cap J) = \\mathrm{zeroLocus}(I) \\cup \\mathrm{zeroLocus}(J).$$$

Lean4

theorem zeroLocus_inf (I J : Ideal R) : zeroLocus ((I ⊓ J : Ideal R) : Set R) = zeroLocus I ∪ zeroLocus J :=
  Set.ext fun x => x.2.inf_le

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