case h_open
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (u : Set (PrimeSpectrum R)), (u ∈ Set.range fun r => ↑(basicOpen r)) → IsOpen u

case h_nhds
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (a : PrimeSpectrum R) (u : Set (PrimeSpectrum R)),
    a ∈ u → IsOpen u → ∃ v, (v ∈ Set.range fun r => ↑(basicOpen r)) ∧ a ∈ v ∧ v ⊆ u
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ TopologicalSpace.IsTopologicalBasis (Set.range fun r => ↑(basicOpen r))
apply TopologicalSpace.isTopologicalBasis_of_open_of_nhds
case h_open.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
⊢ IsOpen ((fun r => ↑(basicOpen r)) r)
case h_open
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (u : Set (PrimeSpectrum R)), (u ∈ Set.range fun r => ↑(basicOpen r)) → IsOpen u
rintro _ ⟨r, rfl⟩
no goals
case h_open.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
⊢ IsOpen ((fun r => ↑(basicOpen r)) r)
exact isOpen_basicOpen
case h_nhds.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
hp : p ∈ U
s : Set R
hs : zeroLocus s = Uᶜ
⊢ ∃ v, (v ∈ Set.range fun r => ↑(basicOpen r)) ∧ p ∈ v ∧ v ⊆ U
case h_nhds
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (a : PrimeSpectrum R) (u : Set (PrimeSpectrum R)),
    a ∈ u → IsOpen u → ∃ v, (v ∈ Set.range fun r => ↑(basicOpen r)) ∧ a ∈ v ∧ v ⊆ u
rintro p U hp ⟨s, hs⟩
case h_nhds.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hp : ∃ a, a ∈ s ∧ ¬a ∈ ↑p.asIdeal
hs : zeroLocus s = Uᶜ
⊢ ∃ v, (v ∈ Set.range fun r => ↑(basicOpen r)) ∧ p ∈ v ∧ v ⊆ U
case h_nhds.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
hp : p ∈ U
s : Set R
hs : zeroLocus s = Uᶜ
⊢ ∃ v, (v ∈ Set.range fun r => ↑(basicOpen r)) ∧ p ∈ v ∧ v ⊆ U
rw [← compl_compl U, Set.mem_compl_iff, ← hs, mem_zeroLocus, Set.not_subset] at hp
case h_nhds.intro.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hs : zeroLocus s = Uᶜ
f : R
hfs : f ∈ s
hfp : ¬f ∈ ↑p.asIdeal
⊢ ∃ v, (v ∈ Set.range fun r => ↑(basicOpen r)) ∧ p ∈ v ∧ v ⊆ U
case h_nhds.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hp : ∃ a, a ∈ s ∧ ¬a ∈ ↑p.asIdeal
hs : zeroLocus s = Uᶜ
⊢ ∃ v, (v ∈ Set.range fun r => ↑(basicOpen r)) ∧ p ∈ v ∧ v ⊆ U
obtain ⟨f, hfs, hfp⟩ := hp
case h_nhds.intro.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hs : zeroLocus s = Uᶜ
f : R
hfs : f ∈ s
hfp : ¬f ∈ ↑p.asIdeal
⊢ ↑(basicOpen f) ⊆ U
case h_nhds.intro.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hs : zeroLocus s = Uᶜ
f : R
hfs : f ∈ s
hfp : ¬f ∈ ↑p.asIdeal
⊢ ∃ v, (v ∈ Set.range fun r => ↑(basicOpen r)) ∧ p ∈ v ∧ v ⊆ U
refine' ⟨basicOpen f, ⟨f, rfl⟩, hfp, _⟩
case h_nhds.intro.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hs : zeroLocus s = Uᶜ
f : R
hfs : f ∈ s
hfp : ¬f ∈ ↑p.asIdeal
⊢ zeroLocus s ⊆ zeroLocus {f}
case h_nhds.intro.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hs : zeroLocus s = Uᶜ
f : R
hfs : f ∈ s
hfp : ¬f ∈ ↑p.asIdeal
⊢ ↑(basicOpen f) ⊆ U
rw [← Set.compl_subset_compl, ← hs, basicOpen_eq_zeroLocus_compl, compl_compl]
no goals
case h_nhds.intro.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hs : zeroLocus s = Uᶜ
f : R
hfs : f ∈ s
hfp : ¬f ∈ ↑p.asIdeal
⊢ zeroLocus s ⊆ zeroLocus {f}
exact zeroLocus_anti_mono (Set.singleton_subset_iff.mpr hfs)