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