Description: Define Hilbert lattice join. See chjval for its value and chjcl for its closure law. Note that we define it over all Hilbert space subsets to allow proving more general theorems. Even for general subsets the join belongs to CH ; see sshjcl . (Contributed by NM, 1-Nov-2000) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | df-chj |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | chj | ||
1 | vx | ||
2 | chba | ||
3 | 2 | cpw | |
4 | vy | ||
5 | cort | ||
6 | 1 | cv | |
7 | 4 | cv | |
8 | 6 7 | cun | |
9 | 8 5 | cfv | |
10 | 9 5 | cfv | |
11 | 1 4 3 3 10 | cmpo | |
12 | 0 11 | wceq |