HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-chj Structured version   Unicode version

Definition df-chj 26204
Description: Define Hilbert lattice join. See chjval 26246 for its value and chjcl 26251 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 26249. (Contributed by NM, 1-Nov-2000.) (New usage is discouraged.)
Assertion
Ref Expression
df-chj  |-  vH  =  ( x  e.  ~P ~H ,  y  e.  ~P ~H  |->  ( _|_ `  ( _|_ `  ( x  u.  y ) ) ) )
Distinct variable group:    x, y

Detailed syntax breakdown of Definition df-chj
StepHypRef Expression
1 chj 25826 . 2  class  vH
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 chil 25812 . . . 4  class  ~H
54cpw 3997 . . 3  class  ~P ~H
62cv 1382 . . . . . 6  class  x
73cv 1382 . . . . . 6  class  y
86, 7cun 3459 . . . . 5  class  ( x  u.  y )
9 cort 25823 . . . . 5  class  _|_
108, 9cfv 5578 . . . 4  class  ( _|_ `  ( x  u.  y
) )
1110, 9cfv 5578 . . 3  class  ( _|_ `  ( _|_ `  (
x  u.  y ) ) )
122, 3, 5, 5, 11cmpt2 6283 . 2  class  ( x  e.  ~P ~H , 
y  e.  ~P ~H  |->  ( _|_ `  ( _|_ `  ( x  u.  y
) ) ) )
131, 12wceq 1383 1  wff  vH  =  ( x  e.  ~P ~H ,  y  e.  ~P ~H  |->  ( _|_ `  ( _|_ `  ( x  u.  y ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  sshjval  26244
  Copyright terms: Public domain W3C validator