∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtSource P]
  {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {ι : Sort u_1} (U : ι → X.Opens),
  iSup U = ⊤ → (∀ (i : ι), P (CategoryTheory.CategoryStruct.comp (U i).ι f)) → P f