A continuity principle involving NN+oo

[jkingdon]

This is all taken from a Mastodon thread by Martin Escardo at https://mathstodon.xyz/@MartinEscardo/112809256762862829

Define a form of continuity on functions from NN+oo to 2o as follows:

NN+oocn = { f e. ( 2o ^m NN+oo ) | E. m e. _om A. n e. _om
   ( m C_ n -> ( f ` n ) = ( f ` ( x e. _om |-> 1o ) ) ) }

Or in words, a function is continuous (in this sense) if there is a natural number such that every value of the function at a greater natural number equals the value of the function at the point at infinity.

Theorem:

_om e. WOmni <-> E. f e. ( 2o ^m NN+oo ) -. f e. NN+oocn

Corollary:

-. _om e. Womni <-> A. f e. ( 2o ^m NN+oo ) -. -. f e. NN+oocn

(follows immediately by https://us.metamath.org/ileuni/notbii.html and https://us.metamath.org/ileuni/alnex.html ).

Interesting constructive theorem:

F e. ( 2o ^m NN+oo ) -> DECID -. F e. NN+oocn

There's a bit more in the thread but it involves additional definitions, so the above would be a good place to start.

There's an agda formalization at https://www.cs.bham.ac.uk/~mhe/TypeTopology/TypeTopology.DecidabilityOfNonContinuity.html#3537