Description: A sequence of functions converges uniformly iff it is uniformly Cauchy, which is to say that for every 0 < x there is a j such that for all j <_ k , m the functions F ( k ) and F ( m ) are uniformly within x of each other on S . (Contributed by Mario Carneiro, 1-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ulmcau.z | |- Z = ( ZZ>= ` M ) |
|
ulmcau.m | |- ( ph -> M e. ZZ ) |
||
ulmcau.s | |- ( ph -> S e. V ) |
||
ulmcau.f | |- ( ph -> F : Z --> ( CC ^m S ) ) |
||
Assertion | ulmcau2 | |- ( ph -> ( F e. dom ( ~~>u ` S ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ulmcau.z | |- Z = ( ZZ>= ` M ) |
|
2 | ulmcau.m | |- ( ph -> M e. ZZ ) |
|
3 | ulmcau.s | |- ( ph -> S e. V ) |
|
4 | ulmcau.f | |- ( ph -> F : Z --> ( CC ^m S ) ) |
|
5 | 1 2 3 4 | ulmcau | |- ( ph -> ( F e. dom ( ~~>u ` S ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) ) |
6 | 1 2 3 4 | ulmcaulem | |- ( ph -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) ) |
7 | 5 6 | bitrd | |- ( ph -> ( F e. dom ( ~~>u ` S ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) ) |