# HG changeset patch
# User immler
# Date 1387210102 -3600
# Node ID 4876fb408c0d0985c8f0bd0eb07c9f79ea48e621
# Parent  54f1ce13c140699c43724b1e86c2eded50a0f578
lemmas about divideR and scaleR

diff -r 54f1ce13c140 -r 4876fb408c0d src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Mon Dec 16 17:08:22 2013 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Mon Dec 16 17:08:22 2013 +0100
@@ -448,6 +448,37 @@
   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a *\<^sub>R c \<le> b *\<^sub>R d"
   by (rule scaleR_mono) (auto intro: order.trans)
 
+lemma pos_le_divideRI:
+  assumes "0 < c"
+  assumes "c *\<^sub>R a \<le> b"
+  shows "a \<le> b /\<^sub>R c"
+proof -
+  from scaleR_left_mono[OF assms(2)] assms(1)
+  have "c *\<^sub>R a /\<^sub>R c \<le> b /\<^sub>R c"
+    by simp
+  with assms show ?thesis
+    by (simp add: scaleR_one scaleR_scaleR inverse_eq_divide)
+qed
+
+lemma pos_le_divideR_eq:
+  assumes "0 < c"
+  shows "a \<le> b /\<^sub>R c \<longleftrightarrow> c *\<^sub>R a \<le> b"
+proof rule
+  assume "a \<le> b /\<^sub>R c"
+  from scaleR_left_mono[OF this] assms
+  have "c *\<^sub>R a \<le> c *\<^sub>R (b /\<^sub>R c)"
+    by simp
+  with assms show "c *\<^sub>R a \<le> b"
+    by (simp add: scaleR_one scaleR_scaleR inverse_eq_divide)
+qed (rule pos_le_divideRI[OF assms])
+
+lemma scaleR_image_atLeastAtMost:
+  "c > 0 \<Longrightarrow> scaleR c ` {x..y} = {c *\<^sub>R x..c *\<^sub>R y}"
+  apply (auto intro!: scaleR_left_mono)
+  apply (rule_tac x = "inverse c *\<^sub>R xa" in image_eqI)
+  apply (simp_all add: pos_le_divideR_eq[symmetric] scaleR_scaleR scaleR_one)
+  done
+
 end
 
 lemma scaleR_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> (x::'a::ordered_real_vector) \<Longrightarrow> 0 \<le> a *\<^sub>R x"