Puzzle 174:

Given \\(g : Y -> X\\) and \\(\Psi(x,y) = x \le g(y)\\), we must show that \\(\Psi\\) is a feasibility relation.

\\( \Psi \\) is a feasibility relation if and only if

\\[\forall x',x : X, y,y' : Y, x'\le x, y \le y', \Psi(x,y) \to \Psi(x',y')\\]

\\(\Psi(x,y)\\) equals, by the definition of Psi:

\\[x \le g(y)\\]

By transitivity and \\(x\le x'\\):

\\[x'\le g(y)\\]

By monotonicity we have

\\[y\le y' \to g(y)\le g(y')\\]

and so

\\[\to x'\le g(y')\\]

which by definition of \\(\Psi\\), equals \\(\Psi(x',y')\\)

Therefor,

\\[\Psi(x,y) \to \Psi(x',y')\\]

QED.

Given \\(g : Y -> X\\) and \\(\Psi(x,y) = x \le g(y)\\), we must show that \\(\Psi\\) is a feasibility relation.

\\( \Psi \\) is a feasibility relation if and only if

\\[\forall x',x : X, y,y' : Y, x'\le x, y \le y', \Psi(x,y) \to \Psi(x',y')\\]

\\(\Psi(x,y)\\) equals, by the definition of Psi:

\\[x \le g(y)\\]

By transitivity and \\(x\le x'\\):

\\[x'\le g(y)\\]

By monotonicity we have

\\[y\le y' \to g(y)\le g(y')\\]

and so

\\[\to x'\le g(y')\\]

which by definition of \\(\Psi\\), equals \\(\Psi(x',y')\\)

Therefor,

\\[\Psi(x,y) \to \Psi(x',y')\\]

QED.