Verma and finite-dimensional weight modules belong to O

Given: The setting above and the hypotheses in the statement.

Fix a finite-dimensional complex semisimple Lie algebra $\mathfrak{g}$, a Cartan subalgebra $\mathfrak{h}$, and a positive Borel $\mathfrak{b}=\mathfrak{h}\oplus {\mathfrak{n}}^{+}$. Write $Q^{+}={\sum }_i{\mathbb{Z}}_{\ge 0}{\alpha }_i$, $\mu \le \lambda$ when $\lambda -\mu \in Q^{+}$, and $w\cdot \lambda =w(\lambda +\rho )-\rho$. The BGG category $\mathcal{O}$ is the full subcategory of left $U(\mathfrak{g})$-modules $M$ satisfying all three conditions: $M$ is finitely generated; $M={⨁}_{\mu \in {\mathfrak{h}}^{\ast }}{M}_{\mu }$ where $M_{\mu }=\{v:hv=\mu (h)v\text{ for all }h\in \mathfrak{h}\}$; and $U({\mathfrak{n}}^{+})v$ is finite dimensional for each $v\in M$. Its morphisms are all $\mathfrak{g}$-linear maps. The zero module is included, generated by the empty set. The enveloping and triangular conventions are those of thm-pbw-ordered-monomial-basis-for-the-enveloping-algebra and thm-triangular-decomposition-from-a-chosen-positive-root-system. (The classical BGG category O)

Fix a finite-dimensional complex semisimple Lie algebra $\mathfrak{g}$, a Cartan subalgebra $\mathfrak{h}$, and a positive Borel $\mathfrak{b}=\mathfrak{h}\oplus {\mathfrak{n}}^{+}$. Write $Q^{+}={\sum }_i{\mathbb{Z}}_{\ge 0}{\alpha }_i$, $\mu \le \lambda$ when $\lambda -\mu \in Q^{+}$, and $w\cdot \lambda =w(\lambda +\rho )-\rho$. Let $M$ be a finitely generated $\mathfrak{h}$-semisimple $\mathfrak{g}$-module. Then $M\in \mathcal{O}$ if and only if $\mathrm{supp}M\subset {\bigcup }_{i=1}^r({\lambda }_i-Q^{+})$ for some finite list of weights. In either case every $M_{\mu }$ is finite dimensional. The list may be empty for $M=0$; finite generation is an independent hypothesis. (The support description of category O with finite generation)

The weights of $M(\lambda )$ are exactly $\lambda -\beta$ for $\beta \in Q^{+}$; every weight space is finite dimensional, and $M(\lambda {)}_{\lambda }=\mathbb{C}{v}_{\lambda }$. (Weights of a Verma module lie below lambda)