Description: Hilbert space distance metric. (Contributed by NM, 13-Sep-2007) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | hilims.1 | โข โ = ( BaseSet โ ๐ ) | |
hilims.2 | โข +โ = ( +๐ฃ โ ๐ ) | ||
hilims.3 | โข ยทโ = ( ยท๐ OLD โ ๐ ) | ||
hilims.5 | โข ยทih = ( ยท๐OLD โ ๐ ) | ||
hilims.8 | โข ๐ท = ( IndMet โ ๐ ) | ||
hilims.9 | โข ๐ โ NrmCVec | ||
Assertion | hilims | โข ๐ท = ( normโ โ โโ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hilims.1 | โข โ = ( BaseSet โ ๐ ) | |
2 | hilims.2 | โข +โ = ( +๐ฃ โ ๐ ) | |
3 | hilims.3 | โข ยทโ = ( ยท๐ OLD โ ๐ ) | |
4 | hilims.5 | โข ยทih = ( ยท๐OLD โ ๐ ) | |
5 | hilims.8 | โข ๐ท = ( IndMet โ ๐ ) | |
6 | hilims.9 | โข ๐ โ NrmCVec | |
7 | 1 2 3 4 6 | hilhhi | โข ๐ = โจ โจ +โ , ยทโ โฉ , normโ โฉ |
8 | 7 5 | hhims2 | โข ๐ท = ( normโ โ โโ ) |