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/e2b79f87-11ac-4797-9818-20975ac23af5n%40googlegroups.com.
