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

Definition df-cnop 25363
Description: Define the set of continuous operators on Hilbert space. For every "epsilon" ( ) there is a "delta" ( ) such that... (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-cnop
Distinct variable group:   , , , ,

Detailed syntax breakdown of Definition df-cnop
StepHypRef Expression
1 ccop 24467 . 2
2 vw . . . . . . . . . . . 12
32cv 1369 . . . . . . . . . . 11
4 vx . . . . . . . . . . . 12
54cv 1369 . . . . . . . . . . 11
6 cmv 24446 . . . . . . . . . . 11
73, 5, 6co 6174 . . . . . . . . . 10
8 cno 24444 . . . . . . . . . 10
97, 8cfv 5500 . . . . . . . . 9
10 vz . . . . . . . . . 10
1110cv 1369 . . . . . . . . 9
12 clt 9503 . . . . . . . . 9
139, 11, 12wbr 4374 . . . . . . . 8
14 vt . . . . . . . . . . . . 13
1514cv 1369 . . . . . . . . . . . 12
163, 15cfv 5500 . . . . . . . . . . 11
175, 15cfv 5500 . . . . . . . . . . 11
1816, 17, 6co 6174 . . . . . . . . . 10
1918, 8cfv 5500 . . . . . . . . 9
20 vy . . . . . . . . . 10
2120cv 1369 . . . . . . . . 9
2219, 21, 12wbr 4374 . . . . . . . 8
2313, 22wi 4 . . . . . . 7
24 chil 24440 . . . . . . 7
2523, 2, 24wral 2792 . . . . . 6
26 crp 11076 . . . . . 6
2725, 10, 26wrex 2793 . . . . 5
2827, 20, 26wral 2792 . . . 4
2928, 4, 24wral 2792 . . 3
30 cmap 7298 . . . 4
3124, 24, 30co 6174 . . 3
3229, 14, 31crab 2796 . 2
331, 32wceq 1370 1
Colors of variables: wff setvar class
This definition is referenced by:  elcnop  25380  hhcno  25427
  Copyright terms: Public domain W3C validator