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

[Paolo Capriotti]

On Sat, Oct 25, 2014 at 4:18 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> And I have an impression that the statement
>
>     question : {P Q : NSet} → setℕ ⊆ (P ⋃ Q) →
>                (¬ isFinite P) ⊎ (¬ isFinite Q)
>
> has not a constructive proof.
>
> Has it?

You're right, it's unprovable.  In fact, from `question` above you can distill a
function:

    h : (ℕ → 2) → 2

such that

    ∀ f : ℕ → 2, ¬ isFinite (f⁻¹ (h f))

Now, `h` cannot be continuous.  In fact, let `m` be the modulus of continuity of
`h` at `λ _ → 0`, and let `f : ℕ → 2` be defined by:

    f n = 0 if n ≤ m
    f n = 1 otherwise

then

    0 = h (λ _ → 0) = h f = 1.

Discontinuous functions are taboo, hence `question` cannot be proved.

Paolo