Definition df-lm 15001

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

Step	Hyp	Ref	Expression
1		clm 14998	. 2 class ~~> t
2		vj	. . 3 setvar j
3		ctop 14808	. . 3 class Top
4		vf	. . . . . . 7 setvar f
5	4	cv 1397	. . . . . 6 class f
6	2	cv 1397	. . . . . . . 8 class j
7	6	cuni 3898	. . . . . . 7 class U. j
8		cc 8090	. . . . . . 7 class CC
9		cpm 6861	. . . . . . 7 class ^pm
10	7, 8, 9	co 6028	. . . . . 6 class ( U. j ^pm CC )
11	5, 10	wcel 2202	. . . . 5 wff f e. ( U. j ^pm CC )
12		vx	. . . . . . 7 setvar x
13	12	cv 1397	. . . . . 6 class x
14	13, 7	wcel 2202	. . . . 5 wff x e. U. j
15		vu	. . . . . . . 8 setvar u
16	12, 15	wel 2203	. . . . . . 7 wff x e. u
17		vy	. . . . . . . . . 10 setvar y
18	17	cv 1397	. . . . . . . . 9 class y
19	15	cv 1397	. . . . . . . . 9 class u
20	5, 18	cres 4733	. . . . . . . . 9 class ( f |` y )
21	18, 19, 20	wf 5329	. . . . . . . 8 wff ( f |` y ) : y --> u
22		cuz 9816	. . . . . . . . 9 class ZZ>=
23	22	crn 4732	. . . . . . . 8 class ran ZZ>=
24	21, 17, 23	wrex 2512	. . . . . . 7 wff E. y e. ran ZZ>= ( f |` y ) : y --> u
25	16, 24	wi 4	. . . . . 6 wff ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u )
26	25, 15, 6	wral 2511	. . . . 5 wff A. u e. j ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u )
27	11, 14, 26	w3a 1005	. . . 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 ) )
28	27, 4, 12	copab 4154	. . 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 ) ) }
29	2, 3, 28	cmpt 4155	. 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 ) ) } )
30	1, 29	wceq 1398	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 ) ) } )

This definition is referenced by:  lmrel  15002  lmrcl  15003  lmfval  15004