Description: Define a function that gives the limits of a function f in the filter sense. (Contributed by Jeff Hankins, 14-Oct-2009)
Ref | Expression | ||
---|---|---|---|
Assertion | df-flf | |- fLimf = ( x e. Top , y e. U. ran Fil |-> ( f e. ( U. x ^m U. y ) |-> ( x fLim ( ( U. x FilMap f ) ` y ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cflf | |- fLimf |
|
1 | vx | |- x |
|
2 | ctop | |- Top |
|
3 | vy | |- y |
|
4 | cfil | |- Fil |
|
5 | 4 | crn | |- ran Fil |
6 | 5 | cuni | |- U. ran Fil |
7 | vf | |- f |
|
8 | 1 | cv | |- x |
9 | 8 | cuni | |- U. x |
10 | cmap | |- ^m |
|
11 | 3 | cv | |- y |
12 | 11 | cuni | |- U. y |
13 | 9 12 10 | co | |- ( U. x ^m U. y ) |
14 | cflim | |- fLim |
|
15 | cfm | |- FilMap |
|
16 | 7 | cv | |- f |
17 | 9 16 15 | co | |- ( U. x FilMap f ) |
18 | 11 17 | cfv | |- ( ( U. x FilMap f ) ` y ) |
19 | 8 18 14 | co | |- ( x fLim ( ( U. x FilMap f ) ` y ) ) |
20 | 7 13 19 | cmpt | |- ( f e. ( U. x ^m U. y ) |-> ( x fLim ( ( U. x FilMap f ) ` y ) ) ) |
21 | 1 3 2 6 20 | cmpo | |- ( x e. Top , y e. U. ran Fil |-> ( f e. ( U. x ^m U. y ) |-> ( x fLim ( ( U. x FilMap f ) ` y ) ) ) ) |
22 | 0 21 | wceq | |- fLimf = ( x e. Top , y e. U. ran Fil |-> ( f e. ( U. x ^m U. y ) |-> ( x fLim ( ( U. x FilMap f ) ` y ) ) ) ) |