Domain theoretic characterisations of quasi-metric completeness in terms of formal balls

We characterise those quasi-metric spaces (X, d) whose poset BX of formal balls satisfies the condition for every (x, r),(y, s) is an element of BX, (x, r) << (y, s) double left right arrow d(x, y) < r - s. (*) From this characterisation, we then deduce that a quasi-metric space (X, d) is Smyth-complete if and only if BX is a dcpo satisfying condition (*). We also give characterisations in terms of formal balls for sequentially Yoneda complete quasi-metric spaces and for Yoneda complete T-1 quasi-metric spaces. Finally, we discuss several properties of the Heckmann quasi-metric on the formal balls of any quasi-metric space.