equal
deleted
inserted
replaced
621 subgoal |
621 subgoal |
622 using \<open>y \<in> X\<close> \<open>dist y b < u\<close> |
622 using \<open>y \<in> X\<close> \<open>dist y b < u\<close> |
623 by (simp add: dist_commute) |
623 by (simp add: dist_commute) |
624 subgoal |
624 subgoal |
625 using \<open>0 < u\<close> \<open>b \<in> X\<close> |
625 using \<open>0 < u\<close> \<open>b \<in> X\<close> |
626 by (simp add: ) |
626 by simp |
627 done |
627 done |
628 also have "(L + 1) * dist y b \<le> e / 2" |
628 also have "(L + 1) * dist y b \<le> e / 2" |
629 using le1 \<open>0 \<le> L\<close> by simp |
629 using le1 \<open>0 \<le> L\<close> by simp |
630 also have "dist (f x b) (f a b) < e / 2" |
630 also have "dist (f x b) (f a b) < e / 2" |
631 by (rule d; fact) |
631 by (rule d; fact) |