How to prove this (corollary of) hyperplane separation theorem? $X$ is a nonempty convex subset of $\mathbb{R}^n$ whose element is $x=\left(x_1,...,x_n\right)$.
The theorem is as follows.
If for each $x\in X$, there is an $i \in \left\{1,...,n\right\}$ such that $x_i>0$,
then there exists $\left(\lambda_1,...,\lambda_n\right)$ where $\lambda_i \geqslant 0$ for all $i$ and $\sum_{i=1}^n \lambda_i=1$, such that
$\lambda \cdot x \geqslant 0$ for all $x\in X$
and $\lambda \cdot x>0$, for some $x \in X$.
I was wondering how to prove it. It looks like it is a corollary of the hyperplane separation theorem. "$\geqslant 0$ for all $x$ and $>0$ for some $x$" is a little bit weird and I do not know whether there is a version of the hyperplane separation theorem that has this form and can be applied to prove it.

 A: This is a tedious elaboration of Fedor Petrov's simple but subtle answer at https://mathoverflow.net/a/428210/31729.
From Rockafellar's "Convex Analysis: Theorem 11.3. Let $C_1,C_2 \subset \mathbb{R}^n$ be non empty convex sets. In order that there exist a hyperplane separating separating $C_1$ and $C_2$ properly, it is necessary & sufficient that
$\operatorname{ri} C_1$ and $\operatorname{ri} C_2$ have no point in common.
Let $N = \{x | x_k \le 0 \text{ for all } k \}$. Let $Y = \operatorname{sp} X$ and $C = Y \cap N$. Since $X$ & $C$ are disjoint the above gives the existence of some non zero functional $\eta$ on $Y$ that separates $C,X$. We can assume that $\eta \le 0$ on $C$ (since $0 \in C$) and $\eta \ge 0$ on $X$.
Since $Y$ is the span of $X$, $Y$ has a basis composed of elements of $X$. Since $\eta \ge 0$ is non zero, it must be strictly greater then zero on at least one of the basis elements.
That is, $\eta(x) >0$ for some $ x \in X$.
All that remains is to show that we can express $\eta (x) = \sum_k \eta_k x_k$ for some $\eta_k \ge 0$. This is the subtle part of Fedor's answer.
Minor digression to review some facts about dual cones & linear functionals.
Since $\mathbb{R}^n$ and $Y$ are Hilbert spaces, we can identify
any linear functional with an element of that space. For example, let $\xi_\eta \in Y$ be the element corresponding to the linear functional $\eta$ so that $\eta(y) = \langle \xi_\eta, y \rangle$. We want to show that $\xi_\eta \ge 0$.
The subtle point of the proof (to me, at least) is the following: Suppose $\lambda$ is a linear functional on $\mathbb{R}^n$, then clearly
$\lambda |_Y$ (the restriction of $\lambda$ to $Y$) is a linear
functional on $Y$ as well. Then $\xi_\lambda$ is not necessarily
equal to $\xi_{\lambda |_Y}$. However, for any $y \in Y$ we have
$\lambda(y) = \langle \xi_\lambda, y \rangle = \langle \xi_{\lambda |_Y}, y \rangle$.
For any set $K$ the dual cone is given by $K^* = \{ x | \langle k, x \rangle \ge 0 \text{ for all } k \in K \}$. Note that the dual is a subset of the relevant ambient Hilbert space.
If $A \subset B$ then $B^* \subset A^*$.
If $K_1,...,K_p$ are any sets, then
$(K_1 \cap \cdots \cap K_p)^* = K_1^* + \cdots + K_p^*$ (see Proof of $\left(K_{1} \cap K_{2}\right)^{*}=K_{1}^{*}+K_{2}^{*}:$ the dual of intersection of convex cones is the sum of their duals).
If $K$ is a closed convex cone then $K^{**} = K$.
If we let $\operatorname{cone} K$ denote the smallest convex cone containing $K$, then we see that for any set $K$ we have $K^{**} = \overline{\operatorname{cone}} K $, the smallest closed convex cone containing $K$.
Also note that for any element
$x$, we have $\{x\}^{**} = \operatorname{cone} \{x\}$, the ray passing through $x$.
Let $e_k(x) = x_k$ be the coordinate functionals. Then I claim that if $y \in Y$ is such that $e_k(y) \ge 0$ for all $k$, then $\eta(y) \ge 0$. Suppose not, then $\eta(y) <0$ and since $y \ge 0$ we see that $-y \le 0$ and so $-y \in C$ and $\eta(-y) >0$ which is a contradiction. Hence we have
$\{\xi_{e_1 |_Y} \}^* \cap \cdots \cap \{ \xi_{e_n |_Y} \}^* \subset \{ \xi_{\eta |_Y} \}^*$.
From above we have
$( \{\xi_{e_1 |_Y} \}^* \cap \cdots \cap \{ \xi_{e_n |_Y} \}^* )^* = \operatorname{cone} \{\xi_{e_1 |_Y}\} + \cdots + \operatorname{cone} \{ \xi_{e_n |_Y} \}$ and so
$\operatorname{cone} \{\xi_{\eta |_Y} \}  \subset \operatorname{cone} \{\xi_{e_1 |_Y}\} + \cdots + \operatorname{cone} \{\xi_{e_n |_Y}\}$. In particular,
we can write $\xi_{\eta |_Y} = \sum_k \eta_k \xi_{e_k |_Y}$ for
some $\eta_k \ge 0$.
Finally, extend $\eta$ to all of $\mathbb{R}^n$ by letting $\eta(x) = \sum_k \eta_k x_k = \langle \sum_k \eta_k \xi_{e_k}, x \rangle $ and note that
$\eta(y) \ge 0$ for all $y \in X$, $\eta(x) \le 0$ for all $x \in N$. Furthermore, there is some $x \in X$ such that $\eta(x) >0$.
To finish, let $\lambda = {1 \over \sum_k \eta_k} \xi_\eta$.
A: Here is an elementary, constructive-ish proof similar to the one given by Iosif Pinelis using the Hyperplane Separation Theorem (HST):
By assumption both $X$ and $Y=ℝ_{≤0}^n$ are non-empty disjoint convex subsets of $V=ℝ^n$. Hence, by the HST, there exists a non-zero vector $v∈ℝ^n$ and scalar $c∈ℝ$ such that
$$∀x∈X:⟨x∣v⟩≥c  \quad\text{and}\quad ∀y∈Y : ⟨y∣v⟩≤c$$
We call such a tuple $(v, c)$ feasible (for both $X$ and $Y$).
Lemma 1: $(v, c)$ is feasible for $Y$ if and only if $c≥0$ and $v∈ℝ_{≥0}^n$, i.e. $v_i≥0$ for all $i$
Proof: $c≥0$ since $0∈Y⟹0=⟨0∣v⟩≤c$. Choosing $y=-αe_i∈ℝ_{≤0}^{n}$, we have $-αv_i =⟨v∣-αe_i⟩≤c$ for all $α>0$, hence $v_i≥0$. On the other hand, if $v∈ℝ_{≥0}^n$ and $c≥0$, then since $Y=ℝ_{≤0}^n$ we have $⟨v∣y⟩≤0≤c$ for all $y∈Y$. ∎
Corollary 1: If $(v, c)$ is feasible, then $(v, 0)$ is feasible
Proof: Since Lemma 1 ensures $c≥0$, we have $⟨v∣x⟩≥c≥0$ for all $x∈X$, so $(v, 0)$ is also feasible for $X$. ∎
From here, we can prove the theorem through recursion
Case 1: There exists some $x∈X$ with $⟨v∣x⟩>0$. Note that if $\dim(V)=1$, then this is guaranteed, since by assumption we'd have $X⊆(0, ∞)$.
Case 2: $⟨v∣x⟩=0$ for all $x∈X$, i.e. $X⊂\operatorname{span}(\{v\})^⟂≕V'$. In this case, reduce the problem to the separation problem in $n-1$ dimensions: $X'≔X∩V'$ and $Y'≔Y ∩ V'$ are both non-empty convex subsets in the linear subspace $V'⊂V$. Note that $X'=X$, since $X⊂V'$.
Thus, by the HST there is a feasible tuple $(v', c')$ for this subproblem. Note that this is not necessarily feasible for the original problem, since we are not guaranteed $⟨v'∣y⟩≤c'$ for all $y∈Y$. However, we can construct a new proposal solution for the original problem through a convex combination:
$$ \tilde{v} = (1-α)v + αv' \qquad \text{and} \qquad \tilde{c} = (1-α)c + αc'$$
We need to prove that this is feasible for the original problem for some $α∈(0,1]$.
Lemma 2: $(v', c')$ is feasible for $Y'$ if and only if $c'≥0$ and if $v_i'≥0$ whenever $v_i=0$
Proof: $c'≥0$ again because $0∈Y'$. If $v_i=0$, then $e_i \perp v$, hence $\operatorname{cone}(-e_i)⊆Y'$, thus $⟨v'∣ -αe_i⟩ = -αv_i'≤c'$ for all $α>0$. Use the same limit argument as in Lemma 1. On the other hand, since $Y'=\operatorname{cone}(\{-e_i∣v_i=0\})$ we have
$$⟨v'∣y'⟩ = \sum_{i: v_i=0} \underbrace{v_i'}_{≥0} \underbrace{y_i'}_{≤0} + \sum_{i: v_i>0} v_i'\underbrace{y_i'}_{=0} ≤ 0 ≤ c' \qquad\text{for all $y'∈Y'$} \qquad ∎$$
Corollary 2: $(\tilde{v}, \tilde{c})$ is feasible for the original problem for some $α∈(0,1]$
Note that any convex combination is feasible for $X$. To get feasibility for $Y$, we need to ensure $\tilde{v}∈ℝ_{≥0}^n$. Using Lemma $2$, we have
$$∀i: (1-α)v_i + αv_i' \overset{!}{≥}0 ⟺ α(v_i-v_i') ≤ v_i \overset{(2)}{⟺} α ≤ \min_{i: v_i≠0} \frac{v_i}{|v_i-v_i'|}∈(0,1] \qquad ∎$$
Now, our new solution either satisfies case (1), or we repeat the argument using $V'=\operatorname{span}(\{v, v'\})^\perp$.

Finally, note that if $(v,0)$ is feasible, then so is the normalized $(λ, 0)$ with $λ = \frac{v}{∑_i v_i} ∈Δ^{n-1}$.

