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

Definition df-hmop 23339
 Description: Define the set of Hermitian operators on Hilbert space. Some books call these "symmetric operators" and others call them "self-adjoint operators," sometimes with slightly different technical meanings. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-hmop
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-hmop
StepHypRef Expression
1 cho 22445 . 2
2 vx . . . . . . . 8
32cv 1651 . . . . . . 7
4 vy . . . . . . . . 9
54cv 1651 . . . . . . . 8
6 vt . . . . . . . . 9
76cv 1651 . . . . . . . 8
85, 7cfv 5446 . . . . . . 7
9 csp 22417 . . . . . . 7
103, 8, 9co 6073 . . . . . 6
113, 7cfv 5446 . . . . . . 7
1211, 5, 9co 6073 . . . . . 6
1310, 12wceq 1652 . . . . 5
14 chil 22414 . . . . 5
1513, 4, 14wral 2697 . . . 4
1615, 2, 14wral 2697 . . 3
17 cmap 7010 . . . 4
1814, 14, 17co 6073 . . 3
1916, 6, 18crab 2701 . 2
201, 19wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  elhmop  23368
 Copyright terms: Public domain W3C validator