# HG changeset patch # User huffman # Date 1179623930 -7200 # Node ID d329182b59660db453f0f779e12b4e3b7a1f9fef # Parent 761f37e0ccc5095723e18625623006cd8deab039 add lemmas LIM_compose2, isCont_LIM_compose2 diff -r 761f37e0ccc5 -r d329182b5966 src/HOL/Hyperreal/Lim.thy --- a/src/HOL/Hyperreal/Lim.thy Sat May 19 19:35:31 2007 +0200 +++ b/src/HOL/Hyperreal/Lim.thy Sun May 20 03:18:50 2007 +0200 @@ -238,6 +238,37 @@ qed qed +lemma LIM_compose2: + assumes f: "f -- a --> b" + assumes g: "g -- b --> c" + assumes inj: "\d>0. \x. x \ a \ norm (x - a) < d \ f x \ b" + shows "(\x. g (f x)) -- a --> c" +proof (rule LIM_I) + fix r :: real + assume r: "0 < r" + obtain s where s: "0 < s" + and less_r: "\y. \y \ b; norm (y - b) < s\ \ norm (g y - c) < r" + using LIM_D [OF g r] by fast + obtain t where t: "0 < t" + and less_s: "\x. \x \ a; norm (x - a) < t\ \ norm (f x - b) < s" + using LIM_D [OF f s] by fast + obtain d where d: "0 < d" + and neq_b: "\x. \x \ a; norm (x - a) < d\ \ f x \ b" + using inj by fast + + show "\t>0. \x. x \ a \ norm (x - a) < t \ norm (g (f x) - c) < r" + proof (safe intro!: exI) + show "0 < min d t" using d t by simp + next + fix x + assume "x \ a" and "norm (x - a) < min d t" + hence "f x \ b" and "norm (f x - b) < s" + using neq_b less_s by simp_all + thus "norm (g (f x) - c) < r" + by (rule less_r) + qed +qed + lemma LIM_o: "\g -- l --> g l; f -- a --> l\ \ (g \ f) -- a --> g l" unfolding o_def by (rule LIM_compose) @@ -468,6 +499,13 @@ "\isCont g l; f -- a --> l\ \ (\x. g (f x)) -- a --> g l" unfolding isCont_def by (rule LIM_compose) +lemma isCont_LIM_compose2: + assumes f [unfolded isCont_def]: "isCont f a" + assumes g: "g -- f a --> l" + assumes inj: "\d>0. \x. x \ a \ norm (x - a) < d \ f x \ f a" + shows "(\x. g (f x)) -- a --> l" +by (rule LIM_compose2 [OF f g inj]) + lemma isCont_o2: "\isCont f a; isCont g (f a)\ \ isCont (\x. g (f x)) a" unfolding isCont_def by (rule LIM_compose)