# HG changeset patch
# User huffman
# Date 1244906974 25200
# Node ID abadaf4922f81576708451a830204fb5e581e204
# Parent  bcb1eb2197f8bf7570d0212f1fed3958de051577
new continuous/vimage lemmas; cleaned up proofs

diff -r bcb1eb2197f8 -r abadaf4922f8 src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Sat Jun 13 08:18:14 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Sat Jun 13 08:29:34 2009 -0700
@@ -3730,6 +3730,16 @@
   shows "(\<forall>x. continuous (at x) f) \<Longrightarrow> closed s ==> closed {x. f x \<in> s}"
   using continuous_closed_preimage[of UNIV f s] closed_UNIV continuous_at_imp_continuous_on by auto
 
+lemma continuous_open_vimage:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
+  shows "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open (f -` s)"
+  unfolding vimage_def by (rule continuous_open_preimage_univ)
+
+lemma continuous_closed_vimage:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
+  shows "\<forall>x. continuous (at x) f \<Longrightarrow> closed s \<Longrightarrow> closed (f -` s)"
+  unfolding vimage_def by (rule continuous_closed_preimage_univ)
+
 text{* Equality of continuous functions on closure and related results.          *}
 
 lemma continuous_closed_in_preimage_constant:
@@ -5164,16 +5174,12 @@
 
 lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
 proof-
-  have *:"{x \<in> UNIV. inner a x \<in> {r. \<exists>x. inner a x = r \<and> r \<le> b}} = {x. inner a x \<le> b}" by auto
-  let ?T = "{..b}"
-  have "closed ?T" by (rule closed_real_atMost)
-  moreover have "{r. \<exists>x. inner a x = r \<and> r \<le> b} = range (inner a) \<inter> ?T"
-    unfolding image_def by auto
-  ultimately have "\<exists>T. closed T \<and> {r. \<exists>x. inner a x = r \<and> r \<le> b} = range (inner a) \<inter> T" by fast
-  hence "closedin euclidean {x \<in> UNIV. inner a x \<in> {r. \<exists>x. inner a x = r \<and> r \<le> b}}"
-    using continuous_on_inner[of UNIV a, unfolded continuous_on_closed subtopology_UNIV] unfolding closedin_closed
-    by (fast elim!: allE[where x="{r. (\<exists>x. inner a x = r \<and> r \<le> b)}"])
-  thus ?thesis unfolding closed_closedin[THEN sym] and * by auto
+  have "\<forall>x. continuous (at x) (inner a)"
+    unfolding continuous_at by (rule allI) (intro tendsto_intros)
+  hence "closed (inner a -` {..b})"
+    using closed_real_atMost by (rule continuous_closed_vimage)
+  moreover have "{x. inner a x \<le> b} = inner a -` {..b}" by auto
+  ultimately show ?thesis by simp
 qed
 
 lemma closed_halfspace_ge: "closed {x. inner a x \<ge> b}"