∀ {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ { carrier := ↥X, str := X.instTopologicalSpaceCarrierCarrier }}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f))
  (V W : (TopologicalSpace.Opens ↥(X.restrict h))ᵒᵖ) (i : V ⟶ W),
  (X.restrict h).presheaf.map i = X.presheaf.map (CategoryTheory.homOfLE ⋯).op