R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
U : Set (PrimeSpectrum R)
⊢ IsOpen U ↔ ∃ s, zeroLocus s = Uᶜ
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
U : Set (PrimeSpectrum R)
⊢ IsOpen U ↔ ∃ s, Uᶜ = zeroLocus s
simp only [@eq_comm _ (Uᶜ)]
no goals
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
U : Set (PrimeSpectrum R)
⊢ IsOpen U ↔ ∃ s, zeroLocus s = Uᶜ
rfl