∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens},
  IsCompact U.carrier →
    IsQuasiSeparated U.carrier →
      ∀ (f : ↑(X.presheaf.obj (Opposite.op U))), IsLocalization.Away f ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))