case h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
f : R
⊢ f ∈ ↑(vanishingIdeal t) ↔ f ∈ {f | ∀ (x : PrimeSpectrum R), x ∈ t → f ∈ x.asIdeal}
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
⊢ ↑(vanishingIdeal t) = {f | ∀ (x : PrimeSpectrum R), x ∈ t → f ∈ x.asIdeal}
ext f
case h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
f : R
⊢ (∀ (i : PrimeSpectrum R), f ∈ ⨅ (_ : i ∈ t), i.asIdeal) ↔ f ∈ {f | ∀ (x : PrimeSpectrum R), x ∈ t → f ∈ x.asIdeal}
case h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
f : R
⊢ f ∈ ↑(vanishingIdeal t) ↔ f ∈ {f | ∀ (x : PrimeSpectrum R), x ∈ t → f ∈ x.asIdeal}
rw [vanishingIdeal, SetLike.mem_coe, Submodule.mem_iInf]
case h.h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
f : R
⊢ ∀ (a : PrimeSpectrum R), (f ∈ ⨅ (_ : a ∈ t), a.asIdeal) ↔ a ∈ t → f ∈ a.asIdeal
case h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
f : R
⊢ (∀ (i : PrimeSpectrum R), f ∈ ⨅ (_ : i ∈ t), i.asIdeal) ↔ f ∈ {f | ∀ (x : PrimeSpectrum R), x ∈ t → f ∈ x.asIdeal}
apply forall_congr'
case h.h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
f : R
x : PrimeSpectrum R
⊢ (f ∈ ⨅ (_ : x ∈ t), x.asIdeal) ↔ x ∈ t → f ∈ x.asIdeal
case h.h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
f : R
⊢ ∀ (a : PrimeSpectrum R), (f ∈ ⨅ (_ : a ∈ t), a.asIdeal) ↔ a ∈ t → f ∈ a.asIdeal
intro x
no goals
case h.h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
f : R
x : PrimeSpectrum R
⊢ (f ∈ ⨅ (_ : x ∈ t), x.asIdeal) ↔ x ∈ t → f ∈ x.asIdeal
rw [Submodule.mem_iInf]