The current definition of df-cau has fewer quantifiers and is also shorter. The switch to using structures is also breaking; I would want to see whether it leads to a shortening in theorems since you might have a raw distance function and wrapping it in a structure might cause issues.
On Sun, Jan 23, 2022 at 10:13 AM Benoit <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/b1475dc5-5b9e-41ed-93d7-72f841be5b82n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSv9egP9YwpSjnpFxheJf-awA0Gu6TO61%3D3OvL0tYduf8g%40mail.gmail.com.
