Theorems · Theorem · algebraic geometry

AlgebraicGeometry.RingedSpace.basicOpen_mul

∀ (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace}
  (f g : ↑(X.presheaf.obj (Opposite.op U))), X.basicOpen (f * g) = X.basicOpen f ⊓ X.basicOpen g

Defined in

Mathlib.Geometry.RingedSpace.Basic

Cited by

2 results in Mathlib

Foundations

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