0006 Function Bounds
Let $A,B,C$ be nonempty sets, $f:A\to B$ and $g:A\times B\to C$.
We define the image of $f$ as
$$ \text{Im}(f) = \{f(d) : d\in A\} $$
For any $d\in A$ we define the $g$ with $d$ fixed to be the function $g_{(d,\cdot)}:B\to C$ defined by
$$ g_{(d,\cdot)}(e) = g(d,e), \quad \forall e\in B $$
For $e\in B$ we define $g$ with $e$ fixed to be $g_{(\cdot,e)}:A\to C$ defined by
$$ g_{(\cdot,e)(d)} = g(d,e),\quad \forall d\in A $$
Either of these is called a partial application of $g$.
Let $A,B$ be nonempty sets and $(X,\preceq)$ a poset, and $f,g:A\to X$ and $h:A\times B \to X$.
We say that $\alpha\in X$ is an upper bound of $f$ if $\alpha\in UB_{\text{Im}(f)}$. We say that $\alpha = \max(f)$ is the maximum of $f$ if $\alpha = \max(\text{Im}(f))$. We say that $\alpha=\sup(f)$ is the supremum of $f$ if $\alpha = \sup(\text{Im}(f))$.
We say that $f\preceq g$ if
$$ f(c)\preceq g(c), \quad \forall c\in A $$
For any $c\in A$ we define the function $\sup_{c\in A}h_{(c,\cdot)}: B\to X$ given by
$$ \left(\sup_{c\in A} h_{(c,\cdot)}\right)(d) = \sup \left( h_{(\cdot,d)}\right), \quad \forall d\in B$$
For any $d\in B$ we define the function $\sup_{d\in B} h_{(\cdot,d)}: A\to X$ given by
$$ \left(\sup_{d\in B} h_{(\cdot,d)}\right)(c) = \sup (h_{(c,\cdot)}),\quad \forall c\in A $$
We use $\sup_{c\in A}\sup_{d\in B}h$ to denote
$$ \sup \left(\sup_{d\in B} h_{(\cdot,d)}\right) $$
and $\sup_{d\in B}\sup_{c\in A}h$ to denote
$$ \sup \left(\sup_{c\in A} h_{(c,\cdot)}\right)$$
Dual defintions and notation for lower bounds, minima, and infima, are all similar.
Throughout this section, assume that $A,B$ are nonempty sets, $(X,\preceq)$ a poset, $f,g:A\to X$ and $h:A\times B\to X$.
Theorem: Fun. Bound Ineq. Sup. Ineq.
Function bounds imply sup bounds.
Statement and proof.
Statement: If $f\preceq g$ and if both $\sup(f)$ and $\sup(g)$ exist, then $\sup f\preceq \sup g$.
Proof: Let $c\in A$, then $f(c)\preceq g(c)\preceq \sup(g)$. Therefore $\sup(g)$ is an upper bound on $f$ and therefore $\sup(f)\preceq \sup(g)$.
$\Box$
Theorem: Fun. Bound Double Sup
Double sups are independent of order.
Statement and proof:
Statement:
$$ \sup h = \sup_{c\in A}\sup_{d\in B} h = \sup_{d\in B}\sup_{c\in A} h $$
Proof: Let $c,d\in A\times B$.
Then $h(c,d) \preceq \left(\sup_{d\in B}h\right)(c) \preceq \sup_{d\in B}\sup_{c\in A} h$.
This shows that $\sup_{d\in B}\sup_{c\in A}h \in UB_{\text{Im}(h)}$.
Now let $\alpha\in UB_{\text{Im}(h)}$.
For every $c\in A,d\in B$ we have $h(c,d)\preceq \alpha$ and therefore
$\alpha$ is an upper bound on $h_{(\cdot,d)}$. Hence $\sup_{c\in A} h_{(c,\cdot)}\preceq \alpha$.
Then $\alpha$ is an upper bound on $\sup_{c\in A} h_{(c,\cdot)}$. Therefore $\sup_{d\in B}\sup_{c\in A}h \preceq \alpha$.
The above shows $\sup_{d\in B}\sup_{c\in A} h = \sup h$.
$\Box$