Theorems · Theorem · algebraic geometry

AlgebraicGeometry.RingedSpace.mem_basicOpen

∀ (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace}
  (f : ↑(X.presheaf.obj (Opposite.op U))) (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U),
  x ∈ X.basicOpen f ↔ IsUnit ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx)) f)

Defined in

Mathlib.Geometry.RingedSpace.Basic

Cited by

8 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound