subset_zeroLocus_vanishingIdeal — Mathlib

English

The vanishing ideal of a set is contained in the ideal of functions that vanish on its zero locus.

Русский

vanishingIdeal множества содержится в идеале функций, которые обращаются в нуль на нулевой локации множества.

LaTeX

$$$t \\subseteq \\mathrm{zeroLocus}(\\mathrm{vanishingIdeal} t)$$$

Lean4

theorem subset_zeroLocus_vanishingIdeal (t : Set (ProjectiveSpectrum 𝒜)) : t ⊆ zeroLocus 𝒜 (vanishingIdeal t) :=
  (gc_ideal _).l_u_le t

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