LLPO: $\forall x \in R (x \ge 0 \vee x \le 0)$.
Is there any known separating theorem following from the LLPO? By separating theorem I mean the separation of a convex, located set Y away from $0$.
So a possible Theorem would be:
Let Y be convex, located and inhabited such that $0 \notin Y$. Then there exists $x \in Y$ such that $\langle x ,y \rangle > 0$ for all $ y \in Y$.
Notice that the separating theorem does not necessarily need to be exactly as formulated above, I am just looking for one in this style.
Also: The proof should be constructive, meaning that the law of excluded middle mustn't be used.
So far I was able to show separating theorems following from the MP ($ \neg (x = 0) \Rightarrow \vert x \vert >0$) and LPO ($\forall x \in \mathbb{R} (x > 0 \vee x = 0 \vee x < 0)$), but I struggle to show something similar with LLPO. My major problem is to make the inequality in the separation strict.