∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtSource P]
  {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {UX : AlgebraicGeometry.Scheme},
  P f → ∀ (i : UX ⟶ X) [AlgebraicGeometry.IsOpenImmersion i], P (CategoryTheory.CategoryStruct.comp i f)