Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-flimfrs Unicode version

Definition df-flimfrs 25682
Description: Gives the limits of a function  f : a --> U. j at a point  p  e.  ( ( cls `  k
) `  a ) relatively to a subspace  a of a topology  k. ( The condition  p  e.  ( ( cls `  k
) `  a ) ensures the traces of the neighborhoods of  p over  a is a filter ( see trnei 17603). The set  a can't be empty since its closure is not empty ( see cldifemp 25627). Experimental. (Contributed by FL, 15-Sep-2013.)
Assertion
Ref Expression
df-flimfrs  |-  fLimfrs  =  ( j  e.  Top , 
k  e.  Top  |->  ( a  e.  ~P U. k  |->  ( p  e.  ( ( cls `  k
) `  a ) ,  f  e.  ( U. j  ^m  a
)  |->  ( ( j 
fLimf  ( ( ( nei `  k ) `  {
p } )t  a ) ) `  f ) ) ) )
Distinct variable group:    j, k, a, p, f

Detailed syntax breakdown of Definition df-flimfrs
StepHypRef Expression
1 cflimfrs 25681 . 2  class  fLimfrs
2 vj . . 3  set  j
3 vk . . 3  set  k
4 ctop 16647 . . 3  class  Top
5 va . . . 4  set  a
63cv 1631 . . . . . 6  class  k
76cuni 3843 . . . . 5  class  U. k
87cpw 3638 . . . 4  class  ~P U. k
9 vp . . . . 5  set  p
10 vf . . . . 5  set  f
115cv 1631 . . . . . 6  class  a
12 ccl 16771 . . . . . . 7  class  cls
136, 12cfv 5271 . . . . . 6  class  ( cls `  k )
1411, 13cfv 5271 . . . . 5  class  ( ( cls `  k ) `
 a )
152cv 1631 . . . . . . 7  class  j
1615cuni 3843 . . . . . 6  class  U. j
17 cmap 6788 . . . . . 6  class  ^m
1816, 11, 17co 5874 . . . . 5  class  ( U. j  ^m  a )
1910cv 1631 . . . . . 6  class  f
209cv 1631 . . . . . . . . . 10  class  p
2120csn 3653 . . . . . . . . 9  class  { p }
22 cnei 16850 . . . . . . . . . 10  class  nei
236, 22cfv 5271 . . . . . . . . 9  class  ( nei `  k )
2421, 23cfv 5271 . . . . . . . 8  class  ( ( nei `  k ) `
 { p }
)
25 crest 13341 . . . . . . . 8  classt
2624, 11, 25co 5874 . . . . . . 7  class  ( ( ( nei `  k
) `  { p } )t  a )
27 cflf 17646 . . . . . . 7  class  fLimf
2815, 26, 27co 5874 . . . . . 6  class  ( j 
fLimf  ( ( ( nei `  k ) `  {
p } )t  a ) )
2919, 28cfv 5271 . . . . 5  class  ( ( j  fLimf  ( (
( nei `  k
) `  { p } )t  a ) ) `
 f )
309, 10, 14, 18, 29cmpt2 5876 . . . 4  class  ( p  e.  ( ( cls `  k ) `  a
) ,  f  e.  ( U. j  ^m  a )  |->  ( ( j  fLimf  ( (
( nei `  k
) `  { p } )t  a ) ) `
 f ) )
315, 8, 30cmpt 4093 . . 3  class  ( a  e.  ~P U. k  |->  ( p  e.  ( ( cls `  k
) `  a ) ,  f  e.  ( U. j  ^m  a
)  |->  ( ( j 
fLimf  ( ( ( nei `  k ) `  {
p } )t  a ) ) `  f ) ) )
322, 3, 4, 4, 31cmpt2 5876 . 2  class  ( j  e.  Top ,  k  e.  Top  |->  ( a  e.  ~P U. k  |->  ( p  e.  ( ( cls `  k
) `  a ) ,  f  e.  ( U. j  ^m  a
)  |->  ( ( j 
fLimf  ( ( ( nei `  k ) `  {
p } )t  a ) ) `  f ) ) ) )
331, 32wceq 1632 1  wff  fLimfrs  =  ( j  e.  Top , 
k  e.  Top  |->  ( a  e.  ~P U. k  |->  ( p  e.  ( ( cls `  k
) `  a ) ,  f  e.  ( U. j  ^m  a
)  |->  ( ( j 
fLimf  ( ( ( nei `  k ) `  {
p } )t  a ) ) `  f ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  islimrs  25683
  Copyright terms: Public domain W3C validator