vanishingIdeal_anti_mono — Mathlib

English

For a given grading 𝒜, if S ⊆ T as sets, then vanishingIdeal(T) ⊆ vanishingIdeal(S) in the homogeneous setting.

Русский

Для данного градуирования 𝒜, если множества S ⊆ T, то vanishingIdeal(T) ⊆ vanishingIdeal(S) в однородном контексте.

LaTeX

$$$S \\subseteq T \\Rightarrow \\mathrm{vanishingIdeal}(T) \\subseteq \\mathrm{vanishingIdeal}(S)$$$

Lean4

theorem vanishingIdeal_anti_mono {s t : Set (ProjectiveSpectrum 𝒜)} (h : s ⊆ t) : vanishingIdeal t ≤ vanishingIdeal s :=
  (gc_ideal _).monotone_u h

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