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
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
