Description: The Cauchy-Schwarz inequality for a subcomplex pre-Hilbert space built from a pre-Hilbert space with certain properties. The main theorem is ipcau . (Contributed by Mario Carneiro, 11-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tcphval.n | |
|
tcphcph.v | |
||
tcphcph.f | |
||
tcphcph.1 | |
||
tcphcph.2 | |
||
tcphcph.h | |
||
tcphcph.3 | |
||
tcphcph.4 | |
||
tcphcph.k | |
||
ipcau2.n | |
||
ipcau2.c | |
||
ipcau2.3 | |
||
ipcau2.4 | |
||
Assertion | ipcau2 | |