Definition. Directed set [dt-0010]

Liam O'Connor

Formally, a non-empty subset $Y \subseteq X$ of a poset $(X,\sqsubseteq )$ is directed iff: $\forall x, y \in Y.\ \exists z \in Y.\ x \sqsubseteq z \land y \sqsubseteq z$

The

z

above is an upper bound of

x

and

y

. Hence, a non-empty set is directed iff every pair of values has an upper bound in the set.

Intuitively, directed sets are "going somewhere" — given two elements we can always find a "greater" one in the set.

Definition. Directed set [dt-0010]

Definition. Directed set [dt-0010]

Example. Power sets are directed [dt-0011]

Theorem. Chain → Directed [dt-0012]

Proof.

Definition. Consistent subset [dt-0013]

Theorem. Alternative characterisation of directedness [dt-0014]

Proof.

Corollary. [dt-0015]

Solution.

Solution.

Solution.

Solution.

Solution.

Solution.

Solution.

Solution.

Proof.

Proof.

Proof.

Proof.

Proof.

Proof.

Definition. Directed set [dt-0010]

Example. Power sets are directed [dt-0011]

Theorem. Chain → Directed [dt-0012]

Proof.

Definition. Consistent subset [dt-0013]

Theorem. Alternative characterisation of directedness [dt-0014]

Proof.

Corollary. [dt-0015]

Proof.

Example. Hoare powerdomain of $\mathbb {N}_\bot$ [dt-0062]

Remark. Angelic nondeterminism [dt-0063]

Proof.

Proof.

Proof.

Proof.