![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > df-chj | Structured version Visualization version Unicode version |
Description: Define Hilbert lattice
join. See chjval 27005 for its value and chjcl 27010 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 ![]() |
Ref | Expression |
---|---|
df-chj |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | chj 26586 |
. 2
![]() ![]() | |
2 | vx |
. . 3
![]() ![]() | |
3 | vy |
. . 3
![]() ![]() | |
4 | chil 26572 |
. . . 4
![]() ![]() | |
5 | 4 | cpw 3951 |
. . 3
![]() ![]() ![]() |
6 | 2 | cv 1443 |
. . . . . 6
![]() ![]() |
7 | 3 | cv 1443 |
. . . . . 6
![]() ![]() |
8 | 6, 7 | cun 3402 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() |
9 | cort 26583 |
. . . . 5
![]() ![]() | |
10 | 8, 9 | cfv 5582 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 10, 9 | cfv 5582 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 2, 3, 5, 5, 11 | cmpt2 6292 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 1, 12 | wceq 1444 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: sshjval 27003 |
Copyright terms: Public domain | W3C validator |