Re: [isabelle] Rearranging equations before taking limits

In regards to my previous reply, I've been working on isolating the problem
and I think it all comes down to the following case.

I can prove:

lemma fixes f :: "real â real"
assumes "continuous_on UNIV f"
shows  "âx. (Îh. f (x+h)) -- 0 --> f x"
using assms win_prob_def
by (metis LIM_offset_zero_iff UNIV_I continuous_on_def)

however if I use an interval S, rather than UNIV, sledgehammer yields so
suggestions. Specifically:

lemma fixes f :: "real â real"
assumes "continuous_on S f"
shows  "âxâS. (Îh. f (x+h)) -- 0 --> f x"

Even adding assumptions such as "Sâ{}" and "SâUNIV" make no difference. How
would I be able to prove the second lemma? Is there some extra which I am

I would really appreciate any help or guidance.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.