Have you already proved the two lemmas you suggested already?
Namely: all singletons are closed, and all closed sets are Borel?
I would suggest proving those two separately first.
On 11 March 2016 at 06:41, Muhammad Qasim <[email protected]> wrote:
> Hello Everyone,
>
> I want to prove the following,
>
> `{PosInf} IN subsets Borel` or
> `{x:extreal} IN subsets Borel`
>
> Since all closed sets belong to Borel sets and all singletons are
> closed sets, it should be provable. I have tried different approaches
> but failed. Can someone suggest a way to prove it in HOL4?
>
> Thank you.
>
> Regards
>
> Qasim
>
>
>
> ------------------------------------------------------------------------------
> Transform Data into Opportunity.
> Accelerate data analysis in your applications with
> Intel Data Analytics Acceleration Library.
> Click to learn more.
> http://pubads.g.doubleclick.net/gampad/clk?id=278785111&iu=/4140
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
Transform Data into Opportunity.
Accelerate data analysis in your applications with
Intel Data Analytics Acceleration Library.
Click to learn more.
http://pubads.g.doubleclick.net/gampad/clk?id=278785111&iu=/4140
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
