src/HOL/Limits.thy
changeset 65036 ab7e11730ad8
parent 64394 141e1ed8d5a0
child 65204 d23eded35a33
     1.1 --- a/src/HOL/Limits.thy	Sun Feb 19 11:58:51 2017 +0100
     1.2 +++ b/src/HOL/Limits.thy	Tue Feb 21 15:04:01 2017 +0000
     1.3 @@ -1696,7 +1696,7 @@
     1.4    unfolding tendsto_def eventually_sequentially
     1.5    by (metis div_le_dividend div_mult_self1_is_m le_trans mult.commute)
     1.6  
     1.7 -lemma Bseq_inverse_lemma: "r \<le> norm x \<Longrightarrow> 0 < r \<Longrightarrow> norm (inverse x) \<le> inverse r"
     1.8 +lemma norm_inverse_le_norm: "r \<le> norm x \<Longrightarrow> 0 < r \<Longrightarrow> norm (inverse x) \<le> inverse r"
     1.9    for x :: "'a::real_normed_div_algebra"
    1.10    apply (subst nonzero_norm_inverse, clarsimp)
    1.11    apply (erule (1) le_imp_inverse_le)