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

Definition df-hmop 23300
 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 22406 . 2
2 vx . . . . . . . 8
32cv 1648 . . . . . . 7
4 vy . . . . . . . . 9
54cv 1648 . . . . . . . 8
6 vt . . . . . . . . 9
76cv 1648 . . . . . . . 8
85, 7cfv 5413 . . . . . . 7
9 csp 22378 . . . . . . 7
103, 8, 9co 6040 . . . . . 6
113, 7cfv 5413 . . . . . . 7
1211, 5, 9co 6040 . . . . . 6
1310, 12wceq 1649 . . . . 5
14 chil 22375 . . . . 5
1513, 4, 14wral 2666 . . . 4
1615, 2, 14wral 2666 . . 3
17 cmap 6977 . . . 4
1814, 14, 17co 6040 . . 3
1916, 6, 18crab 2670 . 2
201, 19wceq 1649 1
 Colors of variables: wff set class This definition is referenced by:  elhmop  23329
 Copyright terms: Public domain W3C validator