equal
deleted
inserted
replaced
68 then have "(r/s) * (v - u) \<le> 1 * (v - u)" |
68 then have "(r/s) * (v - u) \<le> 1 * (v - u)" |
69 by (meson diff_ge_0_iff_ge mult_right_mono \<open>u \<le> v\<close>) |
69 by (meson diff_ge_0_iff_ge mult_right_mono \<open>u \<le> v\<close>) |
70 then show ?thesis |
70 then show ?thesis |
71 by (simp add: field_simps) |
71 by (simp add: field_simps) |
72 qed |
72 qed |
73 |
|
74 declare norm_triangle_ineq4[intro] |
|
75 |
|
76 lemma transitive_stepwise_le: |
|
77 assumes "m \<le> n" "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" and "\<And>n. R n (Suc n)" |
|
78 shows "R m n" |
|
79 using \<open>m \<le> n\<close> |
|
80 by (induction rule: dec_induct) (use assms in blast)+ |
|
81 |
73 |
82 subsection \<open>Some useful lemmas about intervals.\<close> |
74 subsection \<open>Some useful lemmas about intervals.\<close> |
83 |
75 |
84 lemma interior_subset_union_intervals: |
76 lemma interior_subset_union_intervals: |
85 assumes "i = cbox a b" |
77 assumes "i = cbox a b" |