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/50abb4be-3870-4515-9636-52f0213a4b6cn%40googlegroups.com.
