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 ) } )