Description: Properties that determine a pre-Hilbert (inner product) space. (Contributed by Mario Carneiro, 18-Nov-2013) (Revised by Mario Carneiro, 7-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | isphld.v | |
|
isphld.a | |
||
isphld.s | |
||
isphld.i | |
||
isphld.z | |
||
isphld.f | |
||
isphld.k | |
||
isphld.p | |
||
isphld.t | |
||
isphld.c | |
||
isphld.o | |
||
isphld.l | |
||
isphld.r | |
||
isphld.cl | |
||
isphld.d | |
||
isphld.ns | |
||
isphld.cj | |
||
Assertion | isphld | |