Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-nmoo Unicode version

Definition df-nmoo 22234
 Description: Define the norm of an operator between two normed complex vector spaces. This definition produces an operator norm function for each pair of vector spaces . Based on definition of linear operator norm in [AkhiezerGlazman] p. 39, although we define it for all operators for convenience. It isn't necessarily meaningful for nonlinear operators, since it doesn't take into account operator values at vectors with norm greater than 1. See Equation 2 of [Kreyszig] p. 92 for a definition that does (although it ignores the value at the zero vector). However, operator norms are rarely if ever used for nonlinear operators. (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.)
Assertion
Ref Expression
df-nmoo CV CV
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-nmoo
StepHypRef Expression
1 cnmoo 22230 . 2
2 vu . . 3
3 vw . . 3
4 cnv 22051 . . 3
5 vt . . . 4
63cv 1651 . . . . . 6
7 cba 22053 . . . . . 6
86, 7cfv 5445 . . . . 5
92cv 1651 . . . . . 6
109, 7cfv 5445 . . . . 5
11 cmap 7009 . . . . 5
128, 10, 11co 6072 . . . 4
13 vz . . . . . . . . . . 11
1413cv 1651 . . . . . . . . . 10
15 cnmcv 22057 . . . . . . . . . . 11 CV
169, 15cfv 5445 . . . . . . . . . 10 CV
1714, 16cfv 5445 . . . . . . . . 9 CV
18 c1 8980 . . . . . . . . 9
19 cle 9110 . . . . . . . . 9
2017, 18, 19wbr 4204 . . . . . . . 8 CV
21 vx . . . . . . . . . 10
2221cv 1651 . . . . . . . . 9
235cv 1651 . . . . . . . . . . 11
2414, 23cfv 5445 . . . . . . . . . 10
256, 15cfv 5445 . . . . . . . . . 10 CV
2624, 25cfv 5445 . . . . . . . . 9 CV
2722, 26wceq 1652 . . . . . . . 8 CV
2820, 27wa 359 . . . . . . 7 CV CV
2928, 13, 10wrex 2698 . . . . . 6 CV CV
3029, 21cab 2421 . . . . 5 CV CV
31 cxr 9108 . . . . 5
32 clt 9109 . . . . 5
3330, 31, 32csup 7436 . . . 4 CV CV
345, 12, 33cmpt 4258 . . 3 CV CV
352, 3, 4, 4, 34cmpt2 6074 . 2 CV CV
361, 35wceq 1652 1 CV CV
 Colors of variables: wff set class This definition is referenced by:  nmoofval  22251
 Copyright terms: Public domain W3C validator