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

Definition df-leop 22432
 Description: Define positive operator ordering. Definition VI.1 of [Retherford] p. 49. Note that means that is a positive operator. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-leop
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-leop
StepHypRef Expression
1 cleo 21538 . 2
2 vu . . . . . . 7
32cv 1622 . . . . . 6
4 vt . . . . . . 7
54cv 1622 . . . . . 6
6 chod 21520 . . . . . 6
73, 5, 6co 5858 . . . . 5
8 cho 21530 . . . . 5
97, 8wcel 1684 . . . 4
10 cc0 8737 . . . . . 6
11 vx . . . . . . . . 9
1211cv 1622 . . . . . . . 8
1312, 7cfv 5255 . . . . . . 7
14 csp 21502 . . . . . . 7
1513, 12, 14co 5858 . . . . . 6
16 cle 8868 . . . . . 6
1710, 15, 16wbr 4023 . . . . 5
18 chil 21499 . . . . 5
1917, 11, 18wral 2543 . . . 4
209, 19wa 358 . . 3
2120, 4, 2copab 4076 . 2
221, 21wceq 1623 1
 Colors of variables: wff set class This definition is referenced by:  leopg  22702
 Copyright terms: Public domain W3C validator