I would like ask you help with a formal proof concerning lattices. Given a generic lattice $L$, there is a general partial order between the elements ($\sqsubseteq$) and a join (lub) operation $\sqcup$ that, given two elements, always returns the lub between the two elements.
My question concerns vectors that contain the elements of this generic lattice $L$. Given two vector ($V$ and $W$) s.t. both vectors have length $n$. Suppose we have $\forall i$ $V[i]$ $\sqsubseteq$ $W[i]$ (we could say that $V$ $\dot{\sqsubseteq}$ $W$ in component-wise notation).
If I apply the join operator ($\sqcup$) to all the elements contained in $V$ I obtain a value of the lattice ($x$). I can do the same thing by joining all the elements inside $W$ (I obtain the value $y$ of the lattice).
My question is: is always true that $x$ $\sqsubseteq$ $y$ ? If yes, how can I prove it formally?
What you're asking is equivalent to the following question:
The answer is yes, it it very clear that it is so.
To prove it, you can argue by stating that $$x_1 \vee x_2 \leq x_1 \vee y_2 \leq y_1 \vee y_2$$ and proceed in the obvious way for bigger values of $n$.
Formally, you can use an induction process in a straightforward way.
More generally, if $A$ and $B$ are subsets of a lattice such that $\bigvee A,\bigvee B$ exist in that lattice, and if for every $a \in A$ there exist $b \in B$ with $a \leq b$, then $\bigvee A \leq \bigvee B$.
This is just because every upper bound of $B$ is also an upper bound of $A$.
Indeed, if $u$ is an upper bound of $B$ and $a \in A$, then there exists $b \in B$ such that $a \leq b$, whence $a \leq u$.