Show that for $\lambda<0$ we have $\inf(\lambda A)=\lambda \sup(A)$ For $A\subset \mathbb{R}$ and $\lambda \in \mathbb{R}$ let's define:
$$
\lambda A = \{\lambda a: a\in A\}
$$
I have to prove that for $\lambda<0$ and bounded $A$ we have $\inf(\lambda A)=\lambda \sup(A)$ and I'm not sure if my proof is correct.
First, let's notice that $\forall a\in A$ we have:
$$
a\leq \sup(A) \iff \lambda a \geq \lambda \sup(A) \hspace{0.3cm} \text{(because $\lambda$ is negative)}.
$$
If the above holds $\forall \lambda a \in \lambda A$ then:
$$
\inf(\lambda A) \geq \lambda \sup(A).
$$
Now for the other inequality, $\forall \lambda a \in \lambda A$ we have:
$$
\lambda a \geq \inf(\lambda A),
$$
so:
$$
a\leq \frac{1}{\lambda}\inf(\lambda A)
$$
and because above holds $\forall a\in A$, we can write:
$$
\sup(A)\leq \frac{1}{\lambda} \inf(\lambda A)
$$
which is same as:
$$
\lambda \sup(A) \geq \inf(\lambda A)
$$
Thus we showed that:
$$
\lambda \sup(A) \leq \inf(\lambda A) \leq \lambda \sup(A)
$$
so
$$
\lambda \sup(A) = \inf(\lambda A).
$$
Can I prove it this way or is there anything missing? Thanks in advance for any help!
 A: First, here is my direct answer to your question: this proof is structurally fine, but its wording can be improved on two points. First, $\;\forall \lambda a \in \lambda A\;$ is formally incorrect and also confusing: you just mean $\;\forall a \in A\;$.  Second, "If the above holds $\;\forall \ldots\;$" should be "Since the latter inequality holds $\;\forall\ldots\;$".$
\newcommand{\calc}{\begin{align} \quad &}
\newcommand{\op}[1]{\\ #1 \quad & \quad \unicode{x201c}}
\newcommand{\hints}[1]{\mbox{#1} \\ \quad & \quad \phantom{\unicode{x201c}} }
\newcommand{\hint}[1]{\mbox{#1} \unicode{x201d} \\ \quad & }
\newcommand{\endcalc}{\end{align}}
\newcommand{\ref}[1]{\text{(#1)}}\newcommand{\inf}[1]{\text{inf}(#1)}
\newcommand{\sup}[1]{\text{sup}(#1)}\newcommand{\then}{\Rightarrow}
\newcommand{\when}{\Leftarrow}\newcommand{\true}{\text{true}}
\newcommand{\false}{\text{false}}
$
The step that you are trying to express by $\;\forall \lambda a \in \lambda A\;$ is, I think, to use the definition of $\;\lambda A \;$ to get from $$
\langle \forall a : a \in A : \lambda a \ge \ldots \rangle
$$ to the equivalent $$
\langle \forall b : b \in \lambda A : b \ge \ldots \rangle
$$  (I'm using slightly different logic notations from here on, which I find easier to work with.  Hopefully those are not too confusing...)
Below, I'm referring to this step simply as "expand definition of $\;\lambda A\;$".  But there is actually a bit of logic complexity hidden in that step, which I can perhaps most easily illustrate by going from the latter to the former:
$$\calc
    \langle \forall b : b \in \lambda A : b \ge \ldots \rangle
\op=\hint{definition of $\;\lambda A\;$}
    \langle \forall b : \langle \exists a : a \in A : b= \lambda a \rangle : b \ge \ldots \rangle
\op{\tag{*} =}\hint{logic}
    \langle \forall b :: \langle \forall a: a \in A \;\land\; b = \lambda a : b \ge \ldots  \rangle\rangle
\op=\hint{logic: exchange quantifiers}
    \langle \forall a: a \in A : \langle \forall b : b = \lambda a : b \ge \ldots \rangle \rangle
\op=\hint{logic: one-point rule}
    \langle \forall a: a \in A : \lambda a \ge \ldots \rangle
\endcalc$$
Here $\ref{*}$ uses the fact that $\;\langle \exists a :: P(a) \rangle \then Q\;$ is equivalent to $\;\langle \forall a :: P(a) \then Q \rangle\;$ if $\;Q\;$ does not contain a free $\;a\;$.

Now as an illustration of how helpful it is to have simple definitions, and to make them explicit, here is an alternative proof.
The definitions which you (implicitly) used for $\;\sup{A}\;$ and $\;\inf{B}\;$ are that \begin{align}
& \langle \forall a : a \in A : a \le \sup{A} \rangle \\
& \langle \forall a : a \in A : a  \le z \rangle \;\then\; \sup{A} \le z \\
\end{align} and  \begin{align}
& \langle \forall b : b \in B : b \ge \inf{B} \rangle \\
& \langle \forall b : b \in B : b \ge z \rangle \;\then\; \inf{B} \ge z \\
\end{align} for any $\;z\;$, and for any set $\;A\;$ which has a lower bound and $\;B\;$ with an upper bound.
Instead, I propose to use the following equivalent but simpler definitions: for all $\;z\;$, $$
\tag{1}
\sup{A} \leq z \;\equiv\; \langle \forall a : a \in A : a \leq z \rangle
$$ and $$
\tag{2}
z \leq \inf{B} \;\equiv\; \langle \forall b : b \in B : z \leq b \rangle
$$
And as a proof principle, the following is very useful when dealing with upper and lower bounds:
$$
\tag{3}
x = y \;\equiv\; \langle \forall z :: z \le x \;\equiv\; z \le y \rangle
$$
which says that two numbers are equal iff they have the same lower bounds.

Now, to prove $$
\tag{4}
\inf{\lambda A} \;=\; \lambda \sup{A}
$$ for $\;\lambda < 0\;$ and a lower-bounded $\;A\;$, we calculate as follows for any $\;z\;$:
$$\calc
    z \le \inf{\lambda A}
\op=\hint{'expand' $\;\inf{\cdots}\;$ using definition $\ref{2}$}
    \langle \forall b : b \in \lambda A : z \leq b \rangle
\op=\hint{expand definition of $\;\lambda A\;$}
    \langle \forall a : a \in A : z \leq \lambda a \rangle
\op=
      \hints{arithmetic: divide by negative $\;\lambda\;$}
      \hints{-- to prepare for introducing $\;\sup{\cdots}\;$ through $\ref{1}$,}
      \hint{since we are working towards the RHS of $\ref{4}$}
    \langle \forall a : a \in A : a \leq z / \lambda \rangle
\op=\hint{introduce $\;\sup{\cdots}\;$ by definition $\ref{1}$}
    \sup{A} \leq z / \lambda
\op=\hint{arithmetic: multiply by negative $\;\lambda\;$}
    z \leq \lambda \sup{A}
\endcalc$$
By principle $\ref{3}$, this proves $\ref{4}$.
