isRadical_vanishingIdeal — Mathlib

English

For closed t, s ⊆ t if and only if vanishingIdeal t ≤ vanishingIdeal s.

Русский

Для замкнутого t верно: s ⊆ t тогда и только тогда, когда vanishingIdeal t ≤ vanishingIdeal s.

LaTeX

$$$\\text{If } t \\text{ is closed},\\ s \\subseteq t \\iff \\operatorname{vanishingIdeal}(t) \\le \\operatorname{vanishingIdeal}(s)$$$

Lean4

theorem isRadical_vanishingIdeal (s : Set (PrimeSpectrum R)) : (vanishingIdeal s).IsRadical :=
  by
  rw [← vanishingIdeal_closure, ← zeroLocus_vanishingIdeal_eq_closure, vanishingIdeal_zeroLocus_eq_radical]
  apply Ideal.radical_isRadical

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