vanishingIdeal_strict_anti_mono_iff

English

For closed s,t, s ⊂ t iff vanishingIdeal t < vanishingIdeal s.

Русский

Для замкнутых s, t верно: s ⊂ t тогда и только тогда, когда vanishingIdeal(t) < vanishingIdeal(s).

LaTeX

$$$s \\subset t \\iff \\operatorname{vanishingIdeal}(t) < \\operatorname{vanishingIdeal}(s)$$$

Lean4

theorem vanishingIdeal_strict_anti_mono_iff {s t : Set (PrimeSpectrum R)} (hs : IsClosed s) (ht : IsClosed t) :
    s ⊂ t ↔ vanishingIdeal t < vanishingIdeal s := by
  rw [Set.ssubset_def, vanishingIdeal_anti_mono_iff hs, vanishingIdeal_anti_mono_iff ht, lt_iff_le_not_ge]

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