The definition is a bit strange indeed, and the comment could be more
precise. It was probably designed for sequences. It looks like (x \mapsto
sin(2k \pi) ~~>t 0 with this definition.
The best thing would be to derive it from a general notion of limit of
functions between two topological spaces, applied to +\infty in RR* (or in
df-bj-ccbar). In the meantime, it could take the form:
|- ~~>t = ( j e. Top |-> { <. f , x >. | ( f e. ( U. j ^pm RR ) /\ x e. U.
j /\ A. u e. j ( x e. u -> E. y e. RR ( A. x e. dom f ( y < x -> ( f ` x )
e. u ) ) } )
although I would prefer to use topological spaces (df-topsp) instead of
topologies. It would make things clearer. It would something like
(* Define the function which associates with a given topological J space
the relation "f ~~>t x" meaning "the partial function f from RR to J
converges to x at +oo". This can be applied in particular to sequences
with values in J. *)
|- ~~>t = ( j e. TopSp |-> { <. f , x >. | ( f e. ( ( Base ` j ) ^pm RR )
/\ x e. ( Base ` j ) /\ A. u e. ( TopOpen ` j ) ( x e. u -> E. y e. RR ( A.
x e. dom f ( y < x -> ( f ` x ) e. u ) ) } )
Benoît
On Saturday, January 22, 2022 at 3:12:44 PM UTC+1 Glauco wrote:
> The definition ~ df-lm is
>
> |- ~~>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 ) ) } )
>
> thus, it can only be applied to functions partially defined on ` CC `.
>
> But the relation only depends on the behavior of the function on an
> upperset of integers, see ~ lmres
>
> Unless I'm missing something here, I would prefer a definition like ~
> df-clim
>
> |- ~~> = { <. f , y >. | ( y e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. (
> ZZ>= ` j ) ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x ) ) }
>
> where no restriction on the domain of ` f ` is imposed (please, see ~
> climres and compare it to ~ lmres )
>
> In any event, why does ` CC ` even come into play, in ~ df-lm ?
>
>
> Here is a first guess for an alternative ~ df-lm (I've not tried to work
> with it, thus in principle it could be wrong)
>
> |- ~~>t = ( j e. Top |-> { <. f , x >. | ( x e. U. j /\ A. u e. j ( x e. u
> -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( f ` k ) e. u ) ) } )
>
>
> Glauco
>
> p.s.
> with a quick search for " ^pm CC " , ~ df-cau comes up; I've not worked
> much with it, but at first look it rises the same question
>
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/0468ab25-cf0f-4f84-93bc-372de266dd4fn%40googlegroups.com.
