∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} {f : X ⟶ Y}
  (base_open : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f.base)),
  (∀ (U : TopologicalSpace.Opens ↑↑X), CategoryTheory.IsIso (f.c.app (Opposite.op (⋯.functor.obj U)))) →
    AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f