Theorem. Continuity implies monotonicity [dt-001L]

Liam O'Connor

Proof.

Liam O'Connor

Consider two elements $x, y$ of a cpo where $x \sqsubseteq y$ . Then $\{x,y\}$ is directed with a lub of $y$ . By the second condition in Definition [dt-001J], we get $f(y) = f(x) \sqcup f(y)$ which is equivalent to $f(x) \sqsubseteq f(y)$ .

Theorem. Continuity implies monotonicity [dt-001L]

Proof.

Problem. Monotonicity is insufficient [dt-001K]

Definition. Continuity [dt-001J]

Theorem. Continuity implies monotonicity [dt-001L]

Proof.

Example. Monotonic but not continuous [dt-001M]

Exercise. [dt-001N]

Solution.

Theorem. Alternative characterisation of continuity [dt-001O]

Proof.

Thesis.

Exercise. [dt-001W]

Solution.

Theorem. The Kleene fixed point theorem [dt-001P]

Proof.

Definition. The $\textbf {fix}$ operator [dt-001Q]

Exercise. [dt-001S]

Solution.

Solution.

Solution.

Proof.