R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ closure s ⊆ closure t
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ s ⊆ t
rw [← ht.closure_subset_iff, ← ht.closure_eq]
no goals
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ closure s ⊆ closure t
convert ← zeroLocus_anti_mono_ideal h <;> apply zeroLocus_vanishingIdeal_eq_closure