# HG changeset patch
# User hoelzl
# Date 1282909690 -7200
# Node ID c4b809e57fe0e70cdbf9a28b9d251253436755dc
# Parent  8b7c009da23ce490b78c97dfcb9c398935f1d986
preimages of open sets over continuous function are open

diff -r 8b7c009da23c -r c4b809e57fe0 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Aug 27 11:49:06 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Aug 27 13:48:10 2010 +0200
@@ -5027,7 +5027,7 @@
   (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i<DIM('a). ((a$$i \<le> x$$i \<and> x$$i \<le> b$$i) \<or> (b$$i \<le> x$$i \<and> x$$i \<le> a$$i))) \<longrightarrow> x \<in> s)"
 
 lemma is_interval_interval: "is_interval {a .. b::'a::ordered_euclidean_space}" (is ?th1)
-  "is_interval {a<..<b}" (is ?th2) proof - 
+  "is_interval {a<..<b}" (is ?th2) proof -
   have *:"\<And>x y z::real. x < y \<Longrightarrow> y < z \<Longrightarrow> x < z" by auto
   show ?th1 ?th2  unfolding is_interval_def mem_interval Ball_def atLeastAtMost_iff
     by(meson order_trans le_less_trans less_le_trans *)+ qed
@@ -5051,6 +5051,9 @@
 lemma continuous_at_inner: "continuous (at x) (inner a)"
   unfolding continuous_at by (intro tendsto_intros)
 
+lemma continuous_at_euclidean_component[intro!, simp]: "continuous (at x) (\<lambda>x. x $$ i)"
+  unfolding euclidean_component_def by (rule continuous_at_inner)
+
 lemma continuous_on_inner:
   fixes s :: "'a::real_inner set"
   shows "continuous_on s (inner a)"
@@ -5159,6 +5162,9 @@
     by (simp add: closed_def open_halfspace_component_lt)
 qed
 
+lemma open_vimage_euclidean_component: "open S \<Longrightarrow> open ((\<lambda>x. x $$ i) -` S)"
+  by (auto intro!: continuous_open_vimage)
+
 text{* This gives a simple derivation of limit component bounds.                 *}
 
 lemma Lim_component_le: fixes f :: "'a \<Rightarrow> 'b::euclidean_space"