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