Least upper bounds [dt-0016]

DefinitionLeast upper bound [dt-0017]

Let X \subseteq Y be a subset of a poset Y. An element y \in Y is a least upper bound (or lub) for X iff:

  1. It is an upper bound: \forall x \in X.\ x \sqsubseteq y
  2. It is less than any other upper bound: \forall y' \in Y.\ (\forall x \in X. x \sqsubseteq y') \Rightarrow y \sqsubseteq y'
It follows that lubs are unique if they exist. We write the lub of a set X as \bigsqcup X, and usually write x \sqcup y as a shorthand for \bigsqcup \{x,y\}.

CorollaryProperties of \sqcup [dt-0018]

When lubs exist, the binary \sqcup operator is idempotent, commutative, and associative. Also, we have that x \sqsubseteq y iff x \sqcup y = y.

TheoremPointedness via lubs [dt-0019]

A poset Y is pointed iff \bigsqcup \emptyset exists, as the lub of an empty set is just the bottom element in the poset, i.e. \bigsqcup \emptyset = \bot .

Information intuition [dt-001A]

    When the poset Y from Definition [dt-0017] is ordered by our information ordering, the intuition of the lub \bigsqcup X is that it combines all of the information content of all the elements of X but it does not add any additional information (hence least).

    ExampleLubs in the domain \mathbb {B}_\bot \times \mathbb {B}_\bot [dt-001B]

      • (\bot , \mathit {F}) \sqcup (\mathit {T},\bot ) = (\mathit {T},\mathit {F})
      • (\bot , \mathit {F}) \sqcup (\bot ,\bot ) = (\bot ,\mathit {F})
      • (\bot , \mathit {F}) \sqcup (\mathit {T}, \mathit {T}) does not exist.

      Exercise [dt-001C]

        What is the lub operator on subsets X \subseteq \mathbb {N} of the poset (\mathbb {N},\leq )?

        Solution.

          Context

            Fixed points [dt-000U]