Weight multiplicity decreases away from a dominant weight (source code)

= Weight multiplicity decreases away from a dominant weight

If $\mu$ and $\lambda$ are weights of a finite-dimensional representation, $\mu$ is dominant, and $\mu\preceq\lambda$, then
$$
\operatorname{mult}(\mu)\geq\operatorname{mult}(\lambda).
$$
Successively subtract a simple root $\alpha_i$ for which $\langle\lambda,\alpha_i^\vee\rangle>0$ and use injectivity of the corresponding $\mathfrak{sl}_2$ lowering operator.