AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff_of_mem

∀ {X : AlgebraicGeometry.Scheme} {I : X.IdealSheafData} {x : ↥X} {U : ↑X.affineOpens},
  x ∈ ↑U → (x ∈ I.supportSet ↔ x ∈ X.zeroLocus ↑(I.ideal U))

Defined in: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 160 from the axioms · uses propext, Classical.choice, Quot.sound

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement · cited by 53,352
CategoryTheory.Functor.objstatement · cited by 19,642
SetLike.coestatement and proof · cited by 8,199
Oppositestatement · cited by 8,081
Set.Elemstatement and proof · cited by 7,166
Idealstatement · cited by 4,748
TopCat.carrierstatement and proof · cited by 3,184
AlgebraicGeometry.Schemestatement and proof · cited by 2,540
CommRingCatstatement · cited by 2,333
TopologicalSpace.Opensstatement · cited by 2,040
AlgebraicGeometry.PresheafedSpace.carrierstatement and proof · cited by 2,020
AlgebraicGeometry.SheafedSpace.toPresheafedSpacestatement and proof · cited by 1,988

Results whose statement or proof uses this declaration.