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