ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-lm Unicode version

Definition df-lm 12202
Description: Define a function on topologies whose value is the convergence relation for sequences into the given topological space. Although  f is typically a sequence (a function from an upperset of integers) with values in the topological space, it need not be. Note, however, that the limit property concerns only values at integers, so that the real-valued function  ( x  e.  RR  |->  ( sin `  ( pi  x.  x ) ) ) converges to zero (in the standard topology on the reals) with this definition. (Contributed by NM, 7-Sep-2006.)
Assertion
Ref Expression
df-lm  |-  ~~> t  =  ( j  e.  Top  |->  { <. f ,  x >.  |  ( f  e.  ( U. j  ^pm  CC )  /\  x  e. 
U. j  /\  A. u  e.  j  (
x  e.  u  ->  E. y  e.  ran  ZZ>= ( f  |`  y
) : y --> u ) ) } )
Distinct variable group:    f, j, x, y, u

Detailed syntax breakdown of Definition df-lm
StepHypRef Expression
1 clm 12199 . 2  class  ~~> t
2 vj . . 3  setvar  j
3 ctop 12007 . . 3  class  Top
4 vf . . . . . . 7  setvar  f
54cv 1313 . . . . . 6  class  f
62cv 1313 . . . . . . . 8  class  j
76cuni 3702 . . . . . . 7  class  U. j
8 cc 7545 . . . . . . 7  class  CC
9 cpm 6497 . . . . . . 7  class  ^pm
107, 8, 9co 5728 . . . . . 6  class  ( U. j  ^pm  CC )
115, 10wcel 1463 . . . . 5  wff  f  e.  ( U. j  ^pm  CC )
12 vx . . . . . . 7  setvar  x
1312cv 1313 . . . . . 6  class  x
1413, 7wcel 1463 . . . . 5  wff  x  e. 
U. j
15 vu . . . . . . . 8  setvar  u
1612, 15wel 1464 . . . . . . 7  wff  x  e.  u
17 vy . . . . . . . . . 10  setvar  y
1817cv 1313 . . . . . . . . 9  class  y
1915cv 1313 . . . . . . . . 9  class  u
205, 18cres 4501 . . . . . . . . 9  class  ( f  |`  y )
2118, 19, 20wf 5077 . . . . . . . 8  wff  ( f  |`  y ) : y --> u
22 cuz 9228 . . . . . . . . 9  class  ZZ>=
2322crn 4500 . . . . . . . 8  class  ran  ZZ>=
2421, 17, 23wrex 2391 . . . . . . 7  wff  E. y  e.  ran  ZZ>= ( f  |`  y ) : y --> u
2516, 24wi 4 . . . . . 6  wff  ( x  e.  u  ->  E. y  e.  ran  ZZ>= ( f  |`  y ) : y --> u )
2625, 15, 6wral 2390 . . . . 5  wff  A. u  e.  j  ( x  e.  u  ->  E. y  e.  ran  ZZ>= ( f  |`  y ) : y --> u )
2711, 14, 26w3a 945 . . . 4  wff  ( f  e.  ( U. j  ^pm  CC )  /\  x  e.  U. j  /\  A. u  e.  j  (
x  e.  u  ->  E. y  e.  ran  ZZ>= ( f  |`  y
) : y --> u ) )
2827, 4, 12copab 3948 . . 3  class  { <. f ,  x >.  |  ( f  e.  ( U. j  ^pm  CC )  /\  x  e.  U. j  /\  A. u  e.  j  ( x  e.  u  ->  E. y  e.  ran  ZZ>= ( f  |`  y
) : y --> u ) ) }
292, 3, 28cmpt 3949 . 2  class  ( j  e.  Top  |->  { <. f ,  x >.  |  ( f  e.  ( U. j  ^pm  CC )  /\  x  e.  U. j  /\  A. u  e.  j  ( x  e.  u  ->  E. y  e.  ran  ZZ>= ( f  |`  y
) : y --> u ) ) } )
301, 29wceq 1314 1  wff  ~~> t  =  ( j  e.  Top  |->  { <. f ,  x >.  |  ( f  e.  ( U. j  ^pm  CC )  /\  x  e. 
U. j  /\  A. u  e.  j  (
x  e.  u  ->  E. y  e.  ran  ZZ>= ( f  |`  y
) : y --> u ) ) } )
Colors of variables: wff set class
This definition is referenced by:  lmrcl  12203  lmfval  12204
  Copyright terms: Public domain W3C validator