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

[Chun Tian (binghe)]

Cancel this question. Finally I found a way to reduce the original goal to

        ∀n. BIGUNION (IMAGE g (count n)) = BIGUNION (IMAGE f (count n))

but it deeply relies on the definition of g, otherwise it seems impossible.  
Sorry for disturbing.

—Chun

> Il giorno 15 set 2018, alle ore 22:26, Chun Tian (binghe) 
> <binghe.l...@gmail.com> ha scritto:
> 
> 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