Does lub-preservation imply monotonicity?

A function f is continuous exactly when it is

  • monotonic, i.e. d\sqsubseteq d' \Rightarrow f(d)\sqsubseteq f(d'), and
  • lub-preserving, i.e. for any chain d_0\sqsubseteq d_1 \sqsubseteq \dots we have f(\bigsqcup_n d_n) = \bigsqcup_n f(d_n) (call this (1))

We can demonstrate that the first property is implied by the second (and is thus unnecessary) by reasoning as follows. Suppose f is lub-preserving.

Lub-preservation is a property of all chains, so let’s consider the particular chain d \sqsubseteq d'. The lub of this chain is d', so the LHS of (1) becomes f(d'). The RHS is f(d) \sqcup f(d'), and since this is required to be equal to f(d') we can deduce that f(d) \sqsubseteq f(d'). We have deduced monotonicity.

Sadly, the reasoning is invalid. Since \sqcup is a binary operation on chains rather than just sets, it might not be defined for f(d) \sqcup f(d'). We could respond by saying that it must be defined because it’s equal to f(d')! This, however, is dependent on your definition of equality. A perfectly sensible definition of equality between x and y could be: if x and y are defined, then the values at which they are defined are the same. This definition makes x=y vacuously true should either be undefined.

In conclusion: the answer is no; to show continuity we need to show both monotonicity and lub-preservation.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s