General positive semi-definite matrix

Set

 context $n\in\mathbb N$
 definiendum $A \in \mathrm{it}(n)$
 postulate $A \in \mathrm{SquareMatrix}(n,\mathbb C)$
 $x \in \text{ColumnVector}(n,\mathbb C)$
 postulate $A \in \mathrm{SquareMatrix}(n,\mathbb C)$ postulate $x^* A\ x \ge 0$