--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Mon Jan 07 13:08:50 2019 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Mon Jan 07 13:16:33 2019 +0100
@@ -1954,7 +1954,7 @@
simp: euclidean_dist_l2[where 'a='a] cbox_def dist_norm)
-subsection%unimportant\<open>Relating linear images to open/closed/interior/closure\<close>
+subsection%unimportant\<open>Relating linear images to open/closed/interior/closure/connected\<close>
proposition open_surjective_linear_image:
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
@@ -2056,6 +2056,13 @@
shows "interior(uminus ` S) = image uminus (interior S)"
by (simp add: bij_uminus interior_bijective_linear_image linear_uminus)
+lemma connected_linear_image:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
+ assumes "linear f" and "connected s"
+ shows "connected (f ` s)"
+using connected_continuous_image assms linear_continuous_on linear_conv_bounded_linear by blast
+
+
subsection%unimportant \<open>"Isometry" (up to constant bounds) of Injective Linear Map\<close>
proposition injective_imp_isometric: