# Limit Preserving Functions in CPOs

Very short proof that limit preserving functions (continuous functions) on complete partial orders are necessarily monotone.

- 30 July, 2013 -
- Article, Programming Language Theory -
- Tags : analysis, domain theory
- 0 Comments

A complete partial order (hereon cpo) is a partial order such that all monotone chains

has a least upper bound

A continuous function between two cpos and is one that preserves the limit/least upper bound on all monotone chains:

#### Theorem (Monotonicity)

All continuous functions are monotone in the sense that .

**Proof:** For the sake of deriving a contradiction, suppose that there exists some non-monotone continuous function for some pairs of cpos and . Then it must be the case that for some pair of elements , but . Now, consider an -chain

that is -terminal and monotone. Obviously, its least upper bound , but

where

because otherwise . Hence, we can show that

and hence cannot be continuous; a contradiction! Therefore, all continuous functions are monotone.