# 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
missing?
I would really appreciate any help or guidance.
Regards,
Aadish

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