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

Definition df-ulm 19756
Description: Define the uniform convergence of a sequence of functions. Here  F ( ~~> u `  S ) G if  F is a sequence of functions  F ( n ) ,  n  e.  NN defined on  S and  G is a function on  S, and for every  0  <  x there is a  j such that the functions  F ( k ) for  j  <_  k are all uniformly within  x of  G on the domain  S. Compare with df-clim 11962. (Contributed by Mario Carneiro, 26-Feb-2015.)
Assertion
Ref Expression
df-ulm  |-  ~~> u  =  ( s  e.  _V  |->  { <. f ,  y
>.  |  E. n  e.  ZZ  ( f : ( ZZ>= `  n ) --> ( CC  ^m  s
)  /\  y :
s --> CC  /\  A. x  e.  RR+  E. j  e.  ( ZZ>= `  n ) A. k  e.  ( ZZ>=
`  j ) A. z  e.  s  ( abs `  ( ( ( f `  k ) `
 z )  -  ( y `  z
) ) )  < 
x ) } )
Distinct variable group:    f, j, k, n, s, x, y, z

Detailed syntax breakdown of Definition df-ulm
StepHypRef Expression
1 culm 19755 . 2  class  ~~> u
2 vs . . 3  set  s
3 cvv 2788 . . 3  class  _V
4 vn . . . . . . . . 9  set  n
54cv 1622 . . . . . . . 8  class  n
6 cuz 10230 . . . . . . . 8  class  ZZ>=
75, 6cfv 5255 . . . . . . 7  class  ( ZZ>= `  n )
8 cc 8735 . . . . . . . 8  class  CC
92cv 1622 . . . . . . . 8  class  s
10 cmap 6772 . . . . . . . 8  class  ^m
118, 9, 10co 5858 . . . . . . 7  class  ( CC 
^m  s )
12 vf . . . . . . . 8  set  f
1312cv 1622 . . . . . . 7  class  f
147, 11, 13wf 5251 . . . . . 6  wff  f : ( ZZ>= `  n ) --> ( CC  ^m  s
)
15 vy . . . . . . . 8  set  y
1615cv 1622 . . . . . . 7  class  y
179, 8, 16wf 5251 . . . . . 6  wff  y : s --> CC
18 vz . . . . . . . . . . . . . . 15  set  z
1918cv 1622 . . . . . . . . . . . . . 14  class  z
20 vk . . . . . . . . . . . . . . . 16  set  k
2120cv 1622 . . . . . . . . . . . . . . 15  class  k
2221, 13cfv 5255 . . . . . . . . . . . . . 14  class  ( f `
 k )
2319, 22cfv 5255 . . . . . . . . . . . . 13  class  ( ( f `  k ) `
 z )
2419, 16cfv 5255 . . . . . . . . . . . . 13  class  ( y `
 z )
25 cmin 9037 . . . . . . . . . . . . 13  class  -
2623, 24, 25co 5858 . . . . . . . . . . . 12  class  ( ( ( f `  k
) `  z )  -  ( y `  z ) )
27 cabs 11719 . . . . . . . . . . . 12  class  abs
2826, 27cfv 5255 . . . . . . . . . . 11  class  ( abs `  ( ( ( f `
 k ) `  z )  -  (
y `  z )
) )
29 vx . . . . . . . . . . . 12  set  x
3029cv 1622 . . . . . . . . . . 11  class  x
31 clt 8867 . . . . . . . . . . 11  class  <
3228, 30, 31wbr 4023 . . . . . . . . . 10  wff  ( abs `  ( ( ( f `
 k ) `  z )  -  (
y `  z )
) )  <  x
3332, 18, 9wral 2543 . . . . . . . . 9  wff  A. z  e.  s  ( abs `  ( ( ( f `
 k ) `  z )  -  (
y `  z )
) )  <  x
34 vj . . . . . . . . . . 11  set  j
3534cv 1622 . . . . . . . . . 10  class  j
3635, 6cfv 5255 . . . . . . . . 9  class  ( ZZ>= `  j )
3733, 20, 36wral 2543 . . . . . . . 8  wff  A. k  e.  ( ZZ>= `  j ) A. z  e.  s 
( abs `  (
( ( f `  k ) `  z
)  -  ( y `
 z ) ) )  <  x
3837, 34, 7wrex 2544 . . . . . . 7  wff  E. j  e.  ( ZZ>= `  n ) A. k  e.  ( ZZ>=
`  j ) A. z  e.  s  ( abs `  ( ( ( f `  k ) `
 z )  -  ( y `  z
) ) )  < 
x
39 crp 10354 . . . . . . 7  class  RR+
4038, 29, 39wral 2543 . . . . . 6  wff  A. x  e.  RR+  E. j  e.  ( ZZ>= `  n ) A. k  e.  ( ZZ>=
`  j ) A. z  e.  s  ( abs `  ( ( ( f `  k ) `
 z )  -  ( y `  z
) ) )  < 
x
4114, 17, 40w3a 934 . . . . 5  wff  ( f : ( ZZ>= `  n
) --> ( CC  ^m  s )  /\  y : s --> CC  /\  A. x  e.  RR+  E. j  e.  ( ZZ>= `  n ) A. k  e.  ( ZZ>=
`  j ) A. z  e.  s  ( abs `  ( ( ( f `  k ) `
 z )  -  ( y `  z
) ) )  < 
x )
42 cz 10024 . . . . 5  class  ZZ
4341, 4, 42wrex 2544 . . . 4  wff  E. n  e.  ZZ  ( f : ( ZZ>= `  n ) --> ( CC  ^m  s
)  /\  y :
s --> CC  /\  A. x  e.  RR+  E. j  e.  ( ZZ>= `  n ) A. k  e.  ( ZZ>=
`  j ) A. z  e.  s  ( abs `  ( ( ( f `  k ) `
 z )  -  ( y `  z
) ) )  < 
x )
4443, 12, 15copab 4076 . . 3  class  { <. f ,  y >.  |  E. n  e.  ZZ  (
f : ( ZZ>= `  n ) --> ( CC 
^m  s )  /\  y : s --> CC  /\  A. x  e.  RR+  E. j  e.  ( ZZ>= `  n ) A. k  e.  ( ZZ>=
`  j ) A. z  e.  s  ( abs `  ( ( ( f `  k ) `
 z )  -  ( y `  z
) ) )  < 
x ) }
452, 3, 44cmpt 4077 . 2  class  ( s  e.  _V  |->  { <. f ,  y >.  |  E. n  e.  ZZ  (
f : ( ZZ>= `  n ) --> ( CC 
^m  s )  /\  y : s --> CC  /\  A. x  e.  RR+  E. j  e.  ( ZZ>= `  n ) A. k  e.  ( ZZ>=
`  j ) A. z  e.  s  ( abs `  ( ( ( f `  k ) `
 z )  -  ( y `  z
) ) )  < 
x ) } )
461, 45wceq 1623 1  wff  ~~> u  =  ( s  e.  _V  |->  { <. f ,  y
>.  |  E. n  e.  ZZ  ( f : ( ZZ>= `  n ) --> ( CC  ^m  s
)  /\  y :
s --> CC  /\  A. x  e.  RR+  E. j  e.  ( ZZ>= `  n ) A. k  e.  ( ZZ>=
`  j ) A. z  e.  s  ( abs `  ( ( ( f `  k ) `
 z )  -  ( y `  z
) ) )  < 
x ) } )
Colors of variables: wff set class
This definition is referenced by:  ulmrel  19757  ulmval  19759
  Copyright terms: Public domain W3C validator