Description: The uniform limit relation is a relation. (Contributed by Mario Carneiro, 26-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | ulmrel | |- Rel ( ~~>u ` S ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 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 ) } ) |
|
2 | 1 | relmptopab | |- Rel ( ~~>u ` S ) |