equal
deleted
inserted
replaced
72 in if P(x, (x+y)/2) then ((x+y)/2, y) |
72 in if P(x, (x+y)/2) then ((x+y)/2, y) |
73 else (x, (x+y)/2))" |
73 else (x, (x+y)/2))" |
74 |
74 |
75 |
75 |
76 |
76 |
77 section{*Some Purely Standard Proofs*} |
77 subsection{*Some Purely Standard Proofs*} |
78 |
78 |
79 lemma LIM_eq: |
79 lemma LIM_eq: |
80 "f -- a --> L = |
80 "f -- a --> L = |
81 (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)" |
81 (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)" |
82 by (simp add: LIM_def diff_minus) |
82 by (simp add: LIM_def diff_minus) |