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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
