Proposition 1.21 — internal points form a convex set

Let $e_1$ and $e_2$ be internal points of an ensemble space, and let $p\in[0,1]$. The mixture $p e_1+\bar p e_2$ is again internal.

Equivalently, the set of internal points is a convex subset: it contains every finite mixture of its members, since a binary mixture stays inside the set and finite mixtures are iterated binary mixtures.

An internal point is an ensemble that admits every ensemble as a component (Definition 1.20). This is Proposition 1.21. The set of internal points may be empty; the statement does not claim otherwise.

Formalization Note. The witnessing coefficient in the definition of an internal point lies in $(0,1]$, including the endpoint $1$. The proof in the draft writes a strict inequality in one algebraic step; the statement formalized here is the definition and the claim as printed in Proposition 1.21, not the intermediate formula that divides by $1-\lambda$.