Hi Chun,
no, it still does not hold. The problem is that case that "a" might be
infinite and while there is for every element 'e' of 'a' an 'n' with 'e
IN f n' you need arbitrary large ones.
A tiny modification of Ramana's counterexample is
f x := count x
sp := UNIV
a := { n | even n }
Cheers
Thomas
On 18.09.2018 10:25, Chun Tian (binghe) wrote:
> Hi Ramana,
>
> thanks for your help. Sorry, I realized that the case “a = sp” can be
> eliminated from other assumptions, thus I actually have another
> constraint “a ≠ sp” in my original goals:
>
> ∃x. a ⊆ f x
> ------------------------------------
> 4. f 0 = ∅
> 5. ∀i j. i ≤ j ⇒ f i ⊆ f j
> 6. BIGUNION (IMAGE f 𝕌(:num)) = sp
> 21. a ≠ sp
> 23. ∀n. f n ⊆ sp
> 24. a ⊆ sp
>
> in this case your opposite proof doesn’t work any more. Also, I
> replaced the monotonicity of f into another form, I don’t know which
> one is easier to use. The assumption "f 0 = ∅” should be optional, I
> guess.
>
> Now this should be a true statement, right?
>
> —Chun
>
>> Il giorno 18 set 2018, alle ore 01:26, Ramana Kumar
>> <ram...@kumar.id.au <mailto:ram...@kumar.id.au>> ha scritto:
>>
>> I think this is false. Here's a proof of the opposite, with the type
>> of f instantiated to a num set generator:
>>
>> val thm = Q.prove(
>> `¬(
>> ∀(f:num->num->bool) a sp.
>> (f 0 = ∅) ∧
>> (∀n. f n ⊆ f (SUC n)) ∧
>> (∀n. f n ⊆ sp) ∧
>> (BIGUNION (IMAGE f 𝕌(:num)) = sp) ∧
>> (a ⊆ sp) ⇒
>> ∃x. a ⊆ f x)`,
>> rw[]
>> \\ qexists_tac`count`
>> \\ qexists_tac`UNIV`
>> \\ rw[SUBSET_DEF, PULL_EXISTS]
>> >- metis_tac[]
>> >- (
>> rw[Once EXTENSION]
>> \\ qexists_tac`count (SUC x)`
>> \\ rw[] )
>> >- (
>> rw[EXTENSION]
>> \\ qexists_tac`SUC x`
>> \\ rw[] ));
>>
>>
>> On Tue, 18 Sep 2018 at 00:01, Chun Tian (binghe)
>> <binghe.l...@gmail.com <mailto:binghe.l...@gmail.com>> wrote:
>>
>> sorry, I also have this necessary assumption:
>>
>> 5. BIGUNION (IMAGE f 𝕌(:num)) = sp
>>
>> > Il giorno 18 set 2018, alle ore 01:00, Chun Tian (binghe)
>> <binghe.l...@gmail.com <mailto:binghe.l...@gmail.com>> ha scritto:
>> >
>> > Hi,
>> >
>> > I ran into the following goal in the proof of a big theorem:
>> >
>> > ∃x. a ⊆ f x
>> > ------------------------------------
>> > 3. f 0 = ∅
>> > 4. ∀n. f n ⊆ f (SUC n)
>> > 20. ∀n. f n ⊆ sp
>> > 21. a ⊆ sp
>> >
>> > I have an increasing sequence of sets (f n) from empty to the
>> whole space (sp), and I have a single set “a” (⊆ sp). It looks
>> *obvious* that, I can always choose a big enough index x such
>> that (f x) will contain “a”. But how can I make this argument formal?
>> >
>> > thanks,
>> >
>> > Chun
>> >
>>
>> _______________________________________________
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> <mailto: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
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
