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

Definition df-chsup 26962
Description: Define the supremum of a set of Hilbert lattice elements. See chsupval2 27061 for its value. We actually define the supremum for an arbitrary collection of Hilbert space subsets, not just elements of the Hilbert lattice  CH, to allow more general theorems. Even for general subsets the supremum still a Hilbert lattice element; see hsupcl 26990. (Contributed by NM, 9-Dec-2003.) (New usage is discouraged.)
Assertion
Ref Expression
df-chsup  |-  \/H  =  ( x  e.  ~P ~P ~H  |->  ( _|_ `  ( _|_ `  U. x ) ) )

Detailed syntax breakdown of Definition df-chsup
StepHypRef Expression
1 chsup 26585 . 2  class  \/H
2 vx . . 3  setvar  x
3 chil 26570 . . . . 5  class  ~H
43cpw 3981 . . . 4  class  ~P ~H
54cpw 3981 . . 3  class  ~P ~P ~H
62cv 1436 . . . . . 6  class  x
76cuni 4219 . . . . 5  class  U. x
8 cort 26581 . . . . 5  class  _|_
97, 8cfv 5601 . . . 4  class  ( _|_ `  U. x )
109, 8cfv 5601 . . 3  class  ( _|_ `  ( _|_ `  U. x ) )
112, 5, 10cmpt 4482 . 2  class  ( x  e.  ~P ~P ~H  |->  ( _|_ `  ( _|_ `  U. x ) ) )
121, 11wceq 1437 1  wff  \/H  =  ( x  e.  ~P ~P ~H  |->  ( _|_ `  ( _|_ `  U. x ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  hsupval  26985
  Copyright terms: Public domain W3C validator