∀ {X Y X' Y' : AlgebraicGeometry.Scheme} (f : X ⟶ X') (g : Y ⟶ Y') [AlgebraicGeometry.IsOpenImmersion f]
  [AlgebraicGeometry.IsOpenImmersion g], AlgebraicGeometry.IsOpenImmersion (CategoryTheory.Limits.coprod.map f g)