# HG changeset patch
# User huffman
# Date 1313011556 25200
# Node ID 0c9feac80852253733319b28f0031b1ac25b979f
# Parent  ac5cb4c864487e9f91db47bf98accd42c44256fb
simplify proof of lemma bounded_component

diff -r ac5cb4c86448 -r 0c9feac80852 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 10 14:10:52 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 10 14:25:56 2011 -0700
@@ -2228,15 +2228,10 @@
     by auto
 qed
 
-lemma bounded_component: "bounded s \<Longrightarrow>
-  bounded ((\<lambda>x. x $$ i) ` (s::'a::euclidean_space set))"
-unfolding bounded_def
-apply clarify
-apply (rule_tac x="x $$ i" in exI)
-apply (rule_tac x="e" in exI)
-apply clarify
-apply (rule order_trans[OF dist_nth_le],simp)
-done
+lemma bounded_component: "bounded s \<Longrightarrow> bounded ((\<lambda>x. x $$ i) ` s)"
+  apply (erule bounded_linear_image)
+  apply (rule bounded_linear_euclidean_component)
+  done
 
 lemma compact_lemma:
   fixes f :: "nat \<Rightarrow> 'a::euclidean_space"