Definition df-xlim 45824

Description: Define the convergence relation for extended real sequences. (Contributed by Glauco Siliprandi, 5-Feb-2022.)

Assertion

Ref	Expression
df-xlim	⊢ ~~>* = (⇝𝑡‘(ordTop‘ ≤ ))

Detailed syntax breakdown of Definition df-xlim

Step	Hyp	Ref	Expression
1		clsxlim 45823	. 2 class ~~>*
2		cle 11216	. . . 4 class ≤
3		cordt 17469	. . . 4 class ordTop
4	2, 3	cfv 6514	. . 3 class (ordTop‘ ≤ )
5		clm 23120	. . 3 class ⇝𝑡
6	4, 5	cfv 6514	. 2 class (⇝𝑡‘(ordTop‘ ≤ ))
7	1, 6	wceq 1540	1 wff ~~>* = (⇝𝑡‘(ordTop‘ ≤ ))

This definition is referenced by:  xlimrel  45825  xlimres  45826  xlimcl  45827  xlimclim  45829  xlimconst  45830  xlimbr  45832  xlimmnfvlem1  45837  xlimmnfvlem2  45838  xlimpnfvlem1  45841  xlimpnfvlem2  45842  xlimuni  45858  xlimfun  45860