Re: [Agda] ℕ ⊆ P U Q -> ¬ isFinite P or ...

[Paolo Capriotti]

On Mon, Oct 27, 2014 at 8:17 AM, Sergei Meshveliani <mechvel at botik.ru> wrote:
>
> As to your explanation with the continuity matters, I fear of that I am
> not aware of notions.
> Is "2" a set of two elements?

Yes.

> What topology or metric on  ℕ → 2  and  2  is used in a notion of
> continuity for a map in  (ℕ → 2) → 2  ?

The discrete topology on `2`, the product topology on `ℕ → 2`. As a topological
space, `ℕ → 2` is homeomorphic to the Cantor set
(http://en.wikipedia.org/wiki/Cantor_set).

This topology is given by a metric like:

    d(f, f') = Σ_{n = 0}^∞ |f(n) - f'(n)| / 2ⁿ

> What does it mean that  m  is a modulus of continuity for  h  at
> g : ℕ → 2   ?
>
> If it is    \forall g ( |h(g') - h(g)| <= m * |g' - g| ),
>
> then what does it mean  |g' - g| ?

It means that

   ∀ g' . (∀ i ≤ m, g i = g' i) → h(g) = h(g').

A modulus of continuity for `h` at `g` exists if and only if `h` is continuous
in `g`.

Martín Escardó has done a lot of work on this topic. He also wrote a number
of blog posts explaining these ideas. You'll find them easily if you google his
name.

Paolo