fixed typo
authorimmler
Tue, 27 Aug 2019 22:43:19 +0200
changeset 70805 d9a71b41de49
parent 70804 c81ac117afa6
child 70806 15a29f5dccbd
child 70807 895b0110181e
child 70808 191bb458b95c
fixed typo
src/HOL/Analysis/Lipschitz.thy
--- a/src/HOL/Analysis/Lipschitz.thy	Tue Aug 27 22:41:47 2019 +0200
+++ b/src/HOL/Analysis/Lipschitz.thy	Tue Aug 27 22:43:19 2019 +0200
@@ -367,7 +367,7 @@
 
 We give several variations around this statement. This is essentially a connectedness argument.\<close>
 
-lemma locally_lipschitz_imp_lispchitz_aux:
+lemma locally_lipschitz_imp_lipschitz_aux:
   fixes f::"real \<Rightarrow> ('a::metric_space)"
   assumes "a \<le> b"
           "continuous_on {a..b} f"
@@ -407,7 +407,7 @@
   shows "lipschitz_on M {a..b} f"
 proof (rule lipschitz_onI[OF _ \<open>M \<ge> 0\<close>])
   have *: "dist (f t) (f s) \<le> M * (t-s)" if "s \<le> t" "s \<in> {a..b}" "t \<in> {a..b}" for s t
-  proof (rule locally_lipschitz_imp_lispchitz_aux, simp add: \<open>s \<le> t\<close>)
+  proof (rule locally_lipschitz_imp_lipschitz_aux, simp add: \<open>s \<le> t\<close>)
     show "continuous_on {s..t} f" using continuous_on_subset[OF assms(1)] that by auto
     fix x assume "x \<in> {s..<t}"
     then have "x \<in> {a..<b}" using that by auto