I want to know the relationship between the following two definitions of monotone operator:
- An operator $f \in \mathcal{P}(V) \to \mathcal{P}(V)$ is monotone with respect to $V$ if and only if, for all $A, B \subseteq V$, $A \subseteq B$ implies $f(A) \subseteq f(B)$
- Let $(A, \leq)$ be a partial order. An operation $f \in A \to A$ is monotone if and only if $a \leq b$ implies $f(a) \leq f(b)$.
Are these simply equivalent definitions or does one of the definitions subsume the other? If we consider $(\mathcal{P}(V), \subseteq)$ we get a partial order with $f \in \mathcal{P}(V) \to \mathcal{P}(V)$ monotone by the second definition. But then how can we go from the second definition to the first? I suppose we could do this if we could ensure that a function $f \in A \to A$ can be lifted to a function $f \in \mathcal{P}(A) \to \mathcal{P}(A)$, which is monotone by the first definition and that the definitions are only guaranteed to be equivalent when $\leq \;=_{df}\; \subseteq$.
Is the following proof going from 2. to 1. correct?
Suppose $(A, \leq)$ is a partial order and $f \in A \to A$ is monotone. Consider the function $f' \in \mathcal{P}(A) \to \mathcal{P}(A)$ such that, for all $X \subseteq A: f'X = \{f(x) \mid x \in X \}$ and suppose that $X,Y \subseteq A$ and $X \subseteq Y$. Then $f'(X) \subseteq f'(Y)$.