Dear Sir,
I can prove that all singletons are closed intervals but not that all
closed intervals belong to Borel sets.
|- {PosInf} = {x | PosInf <= x /\ x <= Posinf}, (easily proved)
|- {x | Normal a <= x /\ x <= Normal b} IN subsets Borel, (already proven)
|- {x | a <= x /\ x <= b} IN subsets Borel, (problem)
Sincerely,
Qasim
Quoting Ramana Kumar <ramana.ku...@cl.cam.ac.uk>:
> 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 <m_q...@encs.concordia.ca> 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
>> hol-info@lists.sourceforge.net
>> 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=278785231&iu=/4140
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
