Probabilistic Testing Semantics - Semantics of Probabilistic Processes: An Operational Approach - page 80

• t s convex , and
• t s Cauchy closed , that is, it contains all its limit points in the usual Euclidean
metric, and is bounded . 1

We are now ready to generalise Proposition 4.1 in order to compare two sets of
vectors. Here we require one set to be p -closed, which allows us to appeal to the
separation theorem from discrete geometry (cf. Theorem 2.7); Cauchy closure alone
is not enough.

Let A , B be subsets of [0, 1] n ; then we have

Theorem 4.1

: h

h

[0, 1] n

A ≤ Ho B iff ∀ h ∈ · A ≤ · B if B is p-closed, and

[0, 1] n

A ≤ Sm B iff ∀ h ∈ : h · A ≤ h · B if A is p-closed.

Proof We consider first the only-if direction for the Smyth case:

≤ Sm B

A

iff ∀ b ∈ B : ∃ a ∈ A : a ≤ b Definition of ≤ Ho

[0, 1] n implies ∀ h ∈ : ∀ b ∈ B : ∃ a ∈ A : h · a ≤ h · b h ≥ 0

[0, 1] n implies ∀ h ∈ : ∀ b ∈ B : h · A ≤ h · b h · A ≤ h · a

∀ ∈

[0, 1] n

· ≤ ·

implies h : h A h B Definition of infimum .

For the if -direction, we use separating hyperplanes, proving the contrapositive:

A ≤ Sm B

iff ∀ a ∈ A : ¬ ( a ≤ b ) Definition of ≤ Sm ; for some b ∈ B

B =∅ define B : b ∈ R

n

b ≤

iff A ∩ ={ | b }

n , c ∈ R

iff ∃ h ∈ R :

A , b ∈ B :

∀ a ∈

b <c<h

h · · a.

In the last step of the reasoning above, we have used Theorem 2.7 as A is p -closed and
B is convex and Cauchy closed by construction; see Fig. 4.2 . Moreover, without loss
of generality, the inequality can be in the direction shown, else we simply multiply
h , c by

1.
We now argue that h is nonnegative, whence by scaling of h , c we obtain without
loss of generality that h

−

[0, 1] n . Assume for a contradiction that h i < 0. Choose

∈

1

Cauchy closure and boundedness together amount to compactness .