Description: The Hilbert space of the Hilbert Space Explorer is a complex Hilbert space. (Contributed by Steve Rodriguez, 29-Apr-2007) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | hilhl | |- <. <. +h , .h >. , normh >. e. CHilOLD |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqid | |- <. <. +h , .h >. , normh >. = <. <. +h , .h >. , normh >. |
|
| 2 | 1 | hhhl | |- <. <. +h , .h >. , normh >. e. CHilOLD |