Cancel above questions. They're finally proved by myself using FINITE_WEAK_ENUMERATE, FINITE_BIJ_COUNT_EQ, etc. [1]
[infinity_bound_lemma] Theorem
⊢ ∀N m. INFINITE N ⇒ ∃n. m ≤ n ∧ n ∈ N
[infinity_often_lemma] Theorem
⊢ ∀P. ¬(∃N. INFINITE N ∧ ∀n. n ∈ N ⇒ P n) ⇔ ∃m. ∀n. m ≤ n ⇒ ¬P n
(they are related to Borel-Cantelli Lemma in Probability Theory)
Still want to know if there're shorter, more elegant proofs ... and
thanks all the same.
--Chun
[1]
https://github.com/binghe/HOL/blob/Probability-11/src/probability/util_probScript.sml
(line 1595-1638)
Il 15/02/19 20:46, Chun Tian (binghe) ha scritto:
> And also this one:
>
> Given `INFINITE N` and a fixed number `m`, how can I assert the
> existence of another number `n` such that,
>
> m <= n /\ n IN N
>
> i.e. prove that
>
> ``!N m. INFINITE N ==> ?n. m <= n /\ n IN N``
>
> --Chun
>
> Il 15/02/19 20:11, Chun Tian (binghe) ha scritto:
>> Hi,
>>
>> I'm blocked at the following (strange) situation:
>>
>> I have an infinite set of integers (num) in which each integer n
>> satisfies a property P(n):
>>
>> ∃N. INFINITE N ∧ ∀n. n ∈ N ⇒ P n
>>
>> Suppose above proposition is NOT true, how can I derive that, there must
>> exist a number m such that for all n >= m, P(n) does NOT hold? i.e.
>>
>> ?m. !n. m <= n ==> ~(P n)
>>
>> Thanks in advance,
>>
>> Chun Tian
>>
>
signature.asc
Description: OpenPGP digital signature
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
