∀ {J : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)] (i j : J) (k : (k : J) × (k ⟶ i) × (k ⟶ j)),
  AlgebraicGeometry.IsOpenImmersion (F.map k.snd.1)