R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ IsOpen (⋃ (i : ℕ), {x | ¬coeff f i ∈ x.asIdeal})
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ IsOpen (imageOfDf f)
rw [imageOfDf, setOf_exists fun i (x : PrimeSpectrum R) => coeff f i ∉ x.asIdeal]
no goals
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ IsOpen (⋃ (i : ℕ), {x | ¬coeff f i ∈ x.asIdeal})
exact isOpen_iUnion fun i => isOpen_basicOpen