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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
