lemmas about divideR and scaleR
authorimmler
Mon Dec 16 17:08:22 2013 +0100 (2013-12-16)
changeset 547854876fb408c0d
parent 54784 54f1ce13c140
child 54786 5e8bdb42078c
lemmas about divideR and scaleR
src/HOL/Real_Vector_Spaces.thy
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Mon Dec 16 17:08:22 2013 +0100
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Mon Dec 16 17:08:22 2013 +0100
     1.3 @@ -448,6 +448,37 @@
     1.4    "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"
     1.5    by (rule scaleR_mono) (auto intro: order.trans)
     1.6  
     1.7 +lemma pos_le_divideRI:
     1.8 +  assumes "0 < c"
     1.9 +  assumes "c *\<^sub>R a \<le> b"
    1.10 +  shows "a \<le> b /\<^sub>R c"
    1.11 +proof -
    1.12 +  from scaleR_left_mono[OF assms(2)] assms(1)
    1.13 +  have "c *\<^sub>R a /\<^sub>R c \<le> b /\<^sub>R c"
    1.14 +    by simp
    1.15 +  with assms show ?thesis
    1.16 +    by (simp add: scaleR_one scaleR_scaleR inverse_eq_divide)
    1.17 +qed
    1.18 +
    1.19 +lemma pos_le_divideR_eq:
    1.20 +  assumes "0 < c"
    1.21 +  shows "a \<le> b /\<^sub>R c \<longleftrightarrow> c *\<^sub>R a \<le> b"
    1.22 +proof rule
    1.23 +  assume "a \<le> b /\<^sub>R c"
    1.24 +  from scaleR_left_mono[OF this] assms
    1.25 +  have "c *\<^sub>R a \<le> c *\<^sub>R (b /\<^sub>R c)"
    1.26 +    by simp
    1.27 +  with assms show "c *\<^sub>R a \<le> b"
    1.28 +    by (simp add: scaleR_one scaleR_scaleR inverse_eq_divide)
    1.29 +qed (rule pos_le_divideRI[OF assms])
    1.30 +
    1.31 +lemma scaleR_image_atLeastAtMost:
    1.32 +  "c > 0 \<Longrightarrow> scaleR c ` {x..y} = {c *\<^sub>R x..c *\<^sub>R y}"
    1.33 +  apply (auto intro!: scaleR_left_mono)
    1.34 +  apply (rule_tac x = "inverse c *\<^sub>R xa" in image_eqI)
    1.35 +  apply (simp_all add: pos_le_divideR_eq[symmetric] scaleR_scaleR scaleR_one)
    1.36 +  done
    1.37 +
    1.38  end
    1.39  
    1.40  lemma scaleR_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> (x::'a::ordered_real_vector) \<Longrightarrow> 0 \<le> a *\<^sub>R x"