src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 57865 dcfb33c26f50
parent 57514 bdc2c6b40bf2
child 58184 db1381d811ab
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Aug 05 16:21:27 2014 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Aug 05 16:58:19 2014 +0200
     1.3 @@ -7307,27 +7307,27 @@
     1.4  
     1.5  lemma real_affinity_le:
     1.6   "0 < (m::'a::linordered_field) \<Longrightarrow> (m * x + c \<le> y \<longleftrightarrow> x \<le> inverse(m) * y + -(c / m))"
     1.7 -  by (simp add: field_simps inverse_eq_divide)
     1.8 +  by (simp add: field_simps)
     1.9  
    1.10  lemma real_le_affinity:
    1.11   "0 < (m::'a::linordered_field) \<Longrightarrow> (y \<le> m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) \<le> x)"
    1.12 -  by (simp add: field_simps inverse_eq_divide)
    1.13 +  by (simp add: field_simps)
    1.14  
    1.15  lemma real_affinity_lt:
    1.16   "0 < (m::'a::linordered_field) \<Longrightarrow> (m * x + c < y \<longleftrightarrow> x < inverse(m) * y + -(c / m))"
    1.17 -  by (simp add: field_simps inverse_eq_divide)
    1.18 +  by (simp add: field_simps)
    1.19  
    1.20  lemma real_lt_affinity:
    1.21   "0 < (m::'a::linordered_field) \<Longrightarrow> (y < m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) < x)"
    1.22 -  by (simp add: field_simps inverse_eq_divide)
    1.23 +  by (simp add: field_simps)
    1.24  
    1.25  lemma real_affinity_eq:
    1.26   "(m::'a::linordered_field) \<noteq> 0 \<Longrightarrow> (m * x + c = y \<longleftrightarrow> x = inverse(m) * y + -(c / m))"
    1.27 -  by (simp add: field_simps inverse_eq_divide)
    1.28 +  by (simp add: field_simps)
    1.29  
    1.30  lemma real_eq_affinity:
    1.31   "(m::'a::linordered_field) \<noteq> 0 \<Longrightarrow> (y = m * x + c  \<longleftrightarrow> inverse(m) * y + -(c / m) = x)"
    1.32 -  by (simp add: field_simps inverse_eq_divide)
    1.33 +  by (simp add: field_simps)
    1.34  
    1.35  
    1.36  subsection {* Banach fixed point theorem (not really topological...) *}