equal
deleted
inserted
replaced
310 done |
310 done |
311 |
311 |
312 lemma starfun_exp_ge_add_one_self [simp]: "0 \<le> x ==> (1 + x) \<le> ( *f* exp) x" |
312 lemma starfun_exp_ge_add_one_self [simp]: "0 \<le> x ==> (1 + x) \<le> ( *f* exp) x" |
313 apply (cases x) |
313 apply (cases x) |
314 apply (simp add: starfun hypreal_add hypreal_le hypreal_zero_num hypreal_one_num, ultra) |
314 apply (simp add: starfun hypreal_add hypreal_le hypreal_zero_num hypreal_one_num, ultra) |
|
315 apply (erule exp_ge_add_one_self_aux) |
315 done |
316 done |
316 |
317 |
317 (* exp (oo) is infinite *) |
318 (* exp (oo) is infinite *) |
318 lemma starfun_exp_HInfinite: |
319 lemma starfun_exp_HInfinite: |
319 "[| x \<in> HInfinite; 0 \<le> x |] ==> ( *f* exp) x \<in> HInfinite" |
320 "[| x \<in> HInfinite; 0 \<le> x |] ==> ( *f* exp) x \<in> HInfinite" |