I'm blocked at the following goal:

I have a function f returning either 0 or 1.  Now I know the infinite
sum of f is finite, i.e.

        suminf f < PosInf       (or `summable f` speaking reals)

How can I prove the set of {x | f x = 1} is finite, or after certain
index m all the rest f(n) are zeros?

        ∃m. ∀n. m ≤ n ⇒ (f n = 0)

If I use CCONTR_TAC (proof by contradiction), I can easily derive the
following 2 assumptions using results I established in my previous
similar questions:

        INFINITE N
        ∀n. n ∈ N ⇒ (f n = 1)

but still I've no idea how to derive a contradiction with `suminf f <
PosInf` by proving `suminf f = PosInf`...


Chun Tian

Attachment: signature.asc
Description: OpenPGP digital signature

hol-info mailing list

Reply via email to