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>
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> 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
> 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
