vanishingIdeal_anti_mono_iff — Mathlib

English

For a closed t, s ⊆ t is equivalent to vanishingIdeal t ≤ vanishingIdeal s.

Русский

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

LaTeX

$$$s \\subseteq t \\iff \\operatorname{vanishingIdeal}(t) \\le \\operatorname{vanishingIdeal}(s) \\text{ for } ht$$$

Lean4

theorem vanishingIdeal_anti_mono_iff {s t : Set (PrimeSpectrum R)} (ht : IsClosed t) :
    s ⊆ t ↔ vanishingIdeal t ≤ vanishingIdeal s :=
  ⟨vanishingIdeal_anti_mono, fun h => by
    rw [← ht.closure_subset_iff, ← ht.closure_eq]
    convert ← zeroLocus_anti_mono_ideal h <;> apply zeroLocus_vanishingIdeal_eq_closure⟩

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