equal
deleted
inserted
replaced
466 show "F = (\<lambda>h. 0)" |
466 show "F = (\<lambda>h. 0)" |
467 proof |
467 proof |
468 fix h show "F h = 0" |
468 fix h show "F h = 0" |
469 proof (rule ccontr) |
469 proof (rule ccontr) |
470 assume **: "F h \<noteq> 0" |
470 assume **: "F h \<noteq> 0" |
471 then have h: "h \<noteq> 0" |
471 hence h: "h \<noteq> 0" by (clarsimp simp add: F.zero) |
472 by (clarsimp simp add: F.zero) |
472 with ** have "0 < ?r h" by simp |
473 with ** have "0 < ?r h" |
|
474 by (simp add: divide_pos_pos) |
|
475 from LIM_D [OF * this] obtain s where s: "0 < s" |
473 from LIM_D [OF * this] obtain s where s: "0 < s" |
476 and r: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> ?r x < ?r h" by auto |
474 and r: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> ?r x < ?r h" by auto |
477 from dense [OF s] obtain t where t: "0 < t \<and> t < s" .. |
475 from dense [OF s] obtain t where t: "0 < t \<and> t < s" .. |
478 let ?x = "scaleR (t / norm h) h" |
476 let ?x = "scaleR (t / norm h) h" |
479 have "?x \<noteq> 0" and "norm ?x < s" using t h by simp_all |
477 have "?x \<noteq> 0" and "norm ?x < s" using t h by simp_all |