Pre-Hilbert space

Set

 context $V$
 definiendum $\langle\mathcal V,\langle\cdot|\cdot\rangle\rangle \in \mathrm{PreHilbert}(V)$
 context $\mathcal V \in \mathrm{VectorSpace}(V,\mathbb C)$ context $\langle\cdot|\cdot\rangle:V\times V\to \mathbb C$
 $u,v,w\in V$ $a,b\in \mathbb C$
 postulate $\overline{\langle v|w \rangle}=\langle w|v \rangle$ postulate $v \ne 0 \Rightarrow \langle v|v \rangle > 0$ postulate $v = 0 \Rightarrow \langle v|v \rangle = 0$ postulate $\langle u|a\cdot v+b\cdot w \rangle = a\cdot \langle u|v \rangle+b\cdot \langle u|w \rangle$ postulate $\langle a\cdot v+b\cdot w | u \rangle = \overline a\cdot \langle v|u \rangle+\overline b \cdot \langle w|u \rangle$

Discussion

Reference

Wikipedia: Inner product space