This can be proved by contradiction, using the fact that the set of numbers
less than any given number is finite.
val lemB = Q.prove
(`!N m. INFINITE N ==> ?n. m <= n /\ n IN N`,
spose_not_then strip_assume_tac
>> `FINITE (count m)` by metis_tac [FINITE_COUNT]
>> `N SUBSET (count m)`
by (rw_tac set_ss [SUBSET_DEF]
>> `~(m <= x)` by metis_tac []
>> decide_tac)
>> metis_tac [SUBSET_FINITE])
On Fri, Feb 15, 2019 at 1:47 PM Chun Tian (binghe) <binghe.l...@gmail.com>
wrote:
> 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
> >
>
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
