x /\ x <= b} IN subsets Borel, (problem)
Sincerely,
Qasim
Quoting Ramana Kumar :
> 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 Ma
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
Hello Everyone,
A theorem named nn_integral_density' in
Nonnegative_Lebesgue_Integration theory of isabelle. They used induct
to prove it. When applied induct 5 cases where returned. Does someone
know of an alternative in HOL4 ?
I am trying to prove the same theorem in HOL4 i.e.,
`!f g M.
ll give you?
>
> On Tue, Mar 10, 2015 at 6:33 PM, Muhammad Qasim
> wrote:
>
>> Hello Everyone,
>>
>> I saw an inductive_set definition in Isabelle. Is there a way to do
>> such defi
Hello Everyone,
I saw an inductive_set definition in Isabelle. Is there a way to do
such definitions in HOL4?
Thank you.
Regards
Qasim
--
Dive into the World of Parallel Programming The Go Parallel Website, sponsore
Hello,
I am looking for an alternative of WF_INDUCT_TAC for HOL4. I would be
greatful if someone can provide good advice. I found a link for this
tactic but the code is for hol_light.
http://mws.cs.ru.nl/~mptp/hol-flyspeck/trunk/wf.html
Looking forward to your response. Thank you.
Regards
