As for df-cau, I think it is expressed in a complicated way (why use balls,
for instance?). It could be:
|- Cau = ( x e. MetSp |-> { f : NN0 --> ( Base `x ) /\ A. e e. RR+ E. n e.
NN0 E. A. k e. ( ZZ>= ` n ) A. l e. ( ZZ>= ` n ) ( ( f ` k ) ( Metric ` x
) ( f ` l ) ) < e ) } )
(provided there is a "Slot" for the (extended) metric of a metric space).
It might be better to define it for uniform spaces. Maybe one could allow
functions defined on ( ZZ>= ` n ) for n \in ZZ.
Benoît
On Sunday, January 23, 2022 at 3:57:01 PM UTC+1 Benoit wrote:
> 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/b1475dc5-5b9e-41ed-93d7-72f841be5b82n%40googlegroups.com.
