Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-xlim Structured version   Visualization version   GIF version

Definition df-xlim 44146
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
StepHypRef Expression
1 clsxlim 44145 . 2 class ~~>*
2 cle 11195 . . . 4 class
3 cordt 17386 . . . 4 class ordTop
42, 3cfv 6497 . . 3 class (ordTop‘ ≤ )
5 clm 22593 . . 3 class 𝑡
64, 5cfv 6497 . 2 class (⇝𝑡‘(ordTop‘ ≤ ))
71, 6wceq 1542 1 wff ~~>* = (⇝𝑡‘(ordTop‘ ≤ ))
Colors of variables: wff setvar class
This definition is referenced by:  xlimrel  44147  xlimres  44148  xlimcl  44149  xlimclim  44151  xlimconst  44152  xlimbr  44154  xlimmnfvlem1  44159  xlimmnfvlem2  44160  xlimpnfvlem1  44163  xlimpnfvlem2  44164  xlimuni  44180  xlimfun  44182
  Copyright terms: Public domain W3C validator