![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > ax-hilex | Structured version Visualization version Unicode version |
Description: This is our first axiom
for a complex Hilbert space, which is the
foundation for quantum mechanics and quantum field theory. We assume that
there exists a primitive class, ![]() |
Ref | Expression |
---|---|
ax-hilex |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | chil 26628 |
. 2
![]() ![]() | |
2 | cvv 3057 |
. 2
![]() ![]() | |
3 | 1, 2 | wcel 1898 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This axiom is referenced by: hvmulex 26720 hilablo 26869 hhph 26887 hcau 26893 hlimadd 26902 hhcms 26912 issh 26917 shex 26921 hlim0 26944 hhssva 26966 hhsssm 26967 hhssnm 26968 hhshsslem1 26974 hhsscms 26986 ocval 26989 spanval 27042 hsupval 27043 sshjval 27059 sshjval3 27063 pjhfval 27105 pjmfn 27424 pjmf1 27425 hosmval 27444 hommval 27445 hodmval 27446 hfsmval 27447 hfmmval 27448 nmopval 27565 elcnop 27566 ellnop 27567 elunop 27581 elhmop 27582 hmopex 27584 nmfnval 27585 nlfnval 27590 elcnfn 27591 ellnfn 27592 dmadjss 27596 dmadjop 27597 adjeu 27598 adjval 27599 eigvecval 27605 eigvalfval 27606 specval 27607 hhcno 27613 hhcnf 27614 adjeq 27644 brafval 27652 kbfval 27661 adjbdln 27792 rnbra 27816 bra11 27817 leoprf2 27836 ishst 27923 |
Copyright terms: Public domain | W3C validator |