[Hol-info] Prove BIGUNION (IMAGE f 𝕌(:num)) by induction on (count n)?

[Chun Tian (binghe)]

Hi,

I have a need to prove that, for two certain functions f, (g :num->’a set)

        BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num))

Following its informal proof, it seems only possible to prove the following 
result (by induction) first:

        !(n :num). BIGUNION (IMAGE f (count n)) = BIGUNION (IMAGE g (count n))

but once I got this intermediate result, how I can reach to the original 
statement? Is there any other assumption needed for going from finite to 
infinite union?

Thanks,

Chun Tian

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