This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-ulm

Description: Define the uniform convergence of a sequence of functions. Here F ( ~>uS ) 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 . (Contributed by Mario Carneiro, 26-Feb-2015)

Ref Expression
Assertion 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 ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 culm 
 |-  ~~>u
1 vs 
 |-  s
2 cvv 
 |-  _V
3 vf 
 |-  f
4 vy 
 |-  y
5 vn 
 |-  n
6 cz 
 |-  ZZ
7 3 cv 
 |-  f
8 cuz 
 |-  ZZ>=
9 5 cv 
 |-  n
10 9 8 cfv 
 |-  ( ZZ>= ` n )
11 cc 
 |-  CC
12 cmap 
 |-  ^m
13 1 cv 
 |-  s
14 11 13 12 co 
 |-  ( CC ^m s )
15 10 14 7 wf 
 |-  f : ( ZZ>= ` n ) --> ( CC ^m s )
16 4 cv 
 |-  y
17 13 11 16 wf 
 |-  y : s --> CC
18 vx 
 |-  x
19 crp 
 |-  RR+
20 vj 
 |-  j
21 vk 
 |-  k
22 20 cv 
 |-  j
23 22 8 cfv 
 |-  ( ZZ>= ` j )
24 vz 
 |-  z
25 cabs 
 |-  abs
26 21 cv 
 |-  k
27 26 7 cfv 
 |-  ( f ` k )
28 24 cv 
 |-  z
29 28 27 cfv 
 |-  ( ( f ` k ) ` z )
30 cmin 
 |-  -
31 28 16 cfv 
 |-  ( y ` z )
32 29 31 30 co 
 |-  ( ( ( f ` k ) ` z ) - ( y ` z ) )
33 32 25 cfv 
 |-  ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) )
34 clt 
 |-  <
35 18 cv 
 |-  x
36 33 35 34 wbr 
 |-  ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x
37 36 24 13 wral 
 |-  A. z e. s ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x
38 37 21 23 wral 
 |-  A. k e. ( ZZ>= ` j ) A. z e. s ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x
39 38 20 10 wrex 
 |-  E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. s ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x
40 39 18 19 wral 
 |-  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
41 15 17 40 w3a 
 |-  ( 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 41 5 6 wrex 
 |-  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 )
43 42 3 4 copab 
 |-  { <. 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 ) }
44 1 2 43 cmpt 
 |-  ( 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 ) } )
45 0 44 wceq 
 |-  ~~>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 ) } )