Since (/) e. CC is false in set.mm (in real life, it should not even be false, but nonsensical), you can prove ( (/) e. CC -> anything ) so climlimsupcex does not look very useful. Maybe there is something special in the proof, in which case that thing could be extracted to state precisely what you mean.
If a meaningful statement contains the construction ( ZZ>= ` M ) , then there is a good chance that M e. ZZ is needed. In an ideal world, the mere writing of ( ZZ>= ` M ) should require M e. ZZ (with the current definition of ZZ>=; one could imagine a definition making sense for any argument in the extended reals). Benoît On Thursday, January 6, 2022 at 2:54:25 PM UTC+1 Glauco wrote: > Hi Thierry , > > this is the counter example > > climlimsupcex.1 $e |- -. M e. ZZ $. > climlimsupcex.2 $e |- Z = ( ZZ>= ` M ) $. > climlimsupcex.3 $e |- F = (/) $. > $( Counterexample for ~ climlimsup , showing that the first hypothesis > is > needed, if the empty set is a complex number (see ~ 0ncn and its > comment) $) > climlimsupcex $p |- ( (/) e. CC -> ( F : Z --> RR /\ F e. dom ~~> /\ > -. F ~~> ( limsup ` F ) ) ) > > As you can see, there's already a "weird" precondition (/) e. CC , but if > you read the comment for ~ 0ncn you'll immediately see why it's there > > ~ climlimsup is not published yet > > $d F k m x $. $d M k m x $. $d Z k m x $. $d k m ph x $. > climlimsup.1 $e |- ( ph -> M e. ZZ ) $. > climlimsup.2 $e |- Z = ( ZZ>= ` M ) $. > climlimsup.3 $e |- ( ph -> F : Z --> RR ) $. > $( A sequence of real numbers converges if and only if it converges to > its > superior limit. The first hypothesis is needed (see ~ climlimsupcex > for > a counterexample) $) > climlimsup $p |- ( ph -> ( F e. dom ~~> <-> F ~~> ( limsup ` F ) ) ) > $= > > Anyway, for the time being, I'm going to change the counterexample in > > |- ( ( (/) e. CC /\ -. -oo e. CC ) -> ( F : Z --> RR /\ F e. dom ~~> /\ -. > F ~~> ( limsup ` F ) ) ) > > I believe it does the job. > > Thanks everyone for the precious help, as always. > Glauco > > > > Il giorno giovedì 6 gennaio 2022 alle 04:54:19 UTC+1 Thierry Arnoux ha > scritto: > >> There are other definitions of infinity on the complex plane: Benoît has >> for example defined the circle at infinity, with an infinite number of >> points at infinity (see ~ bj-inftyexpidisj >> <http://us2.metamath.org:88/mpeuni/bj-inftyexpidisj.html>), and the >> (single) point at infinity of the complex projective line (~ df-bj-infty >> <http://us2.metamath.org:88/mpeuni/df-bj-infty.html>). These might be >> used as more general versions of infinity, and we could then identify the >> current `+oo` and `-oo` with the corresponding points at infinity in >> direction 0 and π. >> >> Glauco, can you give the actual counter example you tried to prove in the >> first place? >> Isn't it possible to prove it within RR, using `abs`, without any need to >> consider `CC`? >> > -- 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/653ea632-ca06-4f92-90d6-a943237ba6b3n%40googlegroups.com.
