# HG changeset patch
# User immler
# Date 1572463570 14400
# Node ID 82057e7b9ea0ae26bbbfa99f3f4ee5b61964dd4c
# Parent  99eec58dc5516b9bc568be978e08305fc6b4920c
linear is not needed

diff -r 99eec58dc551 -r 82057e7b9ea0 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Mon Oct 28 20:51:38 2019 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Wed Oct 30 15:26:10 2019 -0400
@@ -815,7 +815,7 @@
 lemma subpath_translation: "subpath u v ((\<lambda>x. a + x) \<circ> g) = (\<lambda>x. a + x) \<circ> subpath u v g"
   by (rule ext) (simp add: subpath_def)
 
-lemma subpath_linear_image: "linear f \<Longrightarrow> subpath u v (f \<circ> g) = f \<circ> subpath u v g"
+lemma subpath_image: "subpath u v (f \<circ> g) = f \<circ> subpath u v g"
   by (rule ext) (simp add: subpath_def)
 
 lemma affine_ineq: