1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Aug 15 16:48:05 2011 -0700
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Aug 15 18:35:36 2011 -0700
1.3 @@ -5152,56 +5152,63 @@
1.4
1.5 subsection {* Closure of halfspaces and hyperplanes *}
1.6
1.7 +lemma isCont_open_vimage:
1.8 + assumes "\<And>x. isCont f x" and "open s" shows "open (f -` s)"
1.9 +proof -
1.10 + from assms(1) have "continuous_on UNIV f"
1.11 + unfolding isCont_def continuous_on_def within_UNIV by simp
1.12 + hence "open {x \<in> UNIV. f x \<in> s}"
1.13 + using open_UNIV `open s` by (rule continuous_open_preimage)
1.14 + thus "open (f -` s)"
1.15 + by (simp add: vimage_def)
1.16 +qed
1.17 +
1.18 +lemma isCont_closed_vimage:
1.19 + assumes "\<And>x. isCont f x" and "closed s" shows "closed (f -` s)"
1.20 + using assms unfolding closed_def vimage_Compl [symmetric]
1.21 + by (rule isCont_open_vimage)
1.22 +
1.23 lemma open_Collect_less:
1.24 - fixes f g :: "'a::t2_space \<Rightarrow> real"
1.25 - (* FIXME: generalize to topological_space *)
1.26 - assumes f: "\<And>x. continuous (at x) f"
1.27 - assumes g: "\<And>x. continuous (at x) g"
1.28 + fixes f g :: "'a::topological_space \<Rightarrow> real"
1.29 + assumes f: "\<And>x. isCont f x"
1.30 + assumes g: "\<And>x. isCont g x"
1.31 shows "open {x. f x < g x}"
1.32 proof -
1.33 have "open ((\<lambda>x. g x - f x) -` {0<..})"
1.34 - using continuous_sub [OF g f] open_real_greaterThan
1.35 - by (rule continuous_open_vimage [rule_format])
1.36 + using isCont_diff [OF g f] open_real_greaterThan
1.37 + by (rule isCont_open_vimage)
1.38 also have "((\<lambda>x. g x - f x) -` {0<..}) = {x. f x < g x}"
1.39 by auto
1.40 finally show ?thesis .
1.41 qed
1.42
1.43 lemma closed_Collect_le:
1.44 - fixes f g :: "'a::t2_space \<Rightarrow> real"
1.45 - (* FIXME: generalize to topological_space *)
1.46 - assumes f: "\<And>x. continuous (at x) f"
1.47 - assumes g: "\<And>x. continuous (at x) g"
1.48 + fixes f g :: "'a::topological_space \<Rightarrow> real"
1.49 + assumes f: "\<And>x. isCont f x"
1.50 + assumes g: "\<And>x. isCont g x"
1.51 shows "closed {x. f x \<le> g x}"
1.52 proof -
1.53 have "closed ((\<lambda>x. g x - f x) -` {0..})"
1.54 - using continuous_sub [OF g f] closed_real_atLeast
1.55 - by (rule continuous_closed_vimage [rule_format])
1.56 + using isCont_diff [OF g f] closed_real_atLeast
1.57 + by (rule isCont_closed_vimage)
1.58 also have "((\<lambda>x. g x - f x) -` {0..}) = {x. f x \<le> g x}"
1.59 by auto
1.60 finally show ?thesis .
1.61 qed
1.62
1.63 -lemma continuous_at_Pair: (* TODO: move *)
1.64 - assumes f: "continuous (at x) f"
1.65 - assumes g: "continuous (at x) g"
1.66 - shows "continuous (at x) (\<lambda>x. (f x, g x))"
1.67 - using assms unfolding continuous_at by (rule tendsto_Pair)
1.68 -
1.69 lemma closed_Collect_eq:
1.70 - fixes f g :: "'a::t2_space \<Rightarrow> 'b::t2_space"
1.71 - (* FIXME: generalize 'a to topological_space *)
1.72 - assumes f: "\<And>x. continuous (at x) f"
1.73 - assumes g: "\<And>x. continuous (at x) g"
1.74 + fixes f g :: "'a::topological_space \<Rightarrow> 'b::t2_space"
1.75 + assumes f: "\<And>x. isCont f x"
1.76 + assumes g: "\<And>x. isCont g x"
1.77 shows "closed {x. f x = g x}"
1.78 proof -
1.79 have "open {(x::'b, y::'b). x \<noteq> y}"
1.80 unfolding open_prod_def by (auto dest!: hausdorff)
1.81 hence "closed {(x::'b, y::'b). x = y}"
1.82 unfolding closed_def split_def Collect_neg_eq .
1.83 - with continuous_at_Pair [OF f g]
1.84 + with isCont_Pair [OF f g]
1.85 have "closed ((\<lambda>x. (f x, g x)) -` {(x, y). x = y})"
1.86 - by (rule continuous_closed_vimage [rule_format])
1.87 + by (rule isCont_closed_vimage)
1.88 also have "\<dots> = {x. f x = g x}" by auto
1.89 finally show ?thesis .
1.90 qed
1.91 @@ -5222,41 +5229,37 @@
1.92 unfolding continuous_on by (rule ballI) (intro tendsto_intros)
1.93
1.94 lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
1.95 - by (intro closed_Collect_le continuous_at_inner continuous_const)
1.96 + by (intro closed_Collect_le inner.isCont isCont_const isCont_ident)
1.97
1.98 lemma closed_halfspace_ge: "closed {x. inner a x \<ge> b}"
1.99 - by (intro closed_Collect_le continuous_at_inner continuous_const)
1.100 + by (intro closed_Collect_le inner.isCont isCont_const isCont_ident)
1.101
1.102 lemma closed_hyperplane: "closed {x. inner a x = b}"
1.103 - by (intro closed_Collect_eq continuous_at_inner continuous_const)
1.104 + by (intro closed_Collect_eq inner.isCont isCont_const isCont_ident)
1.105
1.106 lemma closed_halfspace_component_le:
1.107 shows "closed {x::'a::euclidean_space. x$$i \<le> a}"
1.108 - by (intro closed_Collect_le continuous_at_euclidean_component
1.109 - continuous_const)
1.110 + by (intro closed_Collect_le euclidean_component.isCont isCont_const)
1.111
1.112 lemma closed_halfspace_component_ge:
1.113 shows "closed {x::'a::euclidean_space. x$$i \<ge> a}"
1.114 - by (intro closed_Collect_le continuous_at_euclidean_component
1.115 - continuous_const)
1.116 + by (intro closed_Collect_le euclidean_component.isCont isCont_const)
1.117
1.118 text {* Openness of halfspaces. *}
1.119
1.120 lemma open_halfspace_lt: "open {x. inner a x < b}"
1.121 - by (intro open_Collect_less continuous_at_inner continuous_const)
1.122 + by (intro open_Collect_less inner.isCont isCont_const isCont_ident)
1.123
1.124 lemma open_halfspace_gt: "open {x. inner a x > b}"
1.125 - by (intro open_Collect_less continuous_at_inner continuous_const)
1.126 + by (intro open_Collect_less inner.isCont isCont_const isCont_ident)
1.127
1.128 lemma open_halfspace_component_lt:
1.129 shows "open {x::'a::euclidean_space. x$$i < a}"
1.130 - by (intro open_Collect_less continuous_at_euclidean_component
1.131 - continuous_const)
1.132 + by (intro open_Collect_less euclidean_component.isCont isCont_const)
1.133
1.134 lemma open_halfspace_component_gt:
1.135 - shows "open {x::'a::euclidean_space. x$$i > a}"
1.136 - by (intro open_Collect_less continuous_at_euclidean_component
1.137 - continuous_const)
1.138 + shows "open {x::'a::euclidean_space. x$$i > a}"
1.139 + by (intro open_Collect_less euclidean_component.isCont isCont_const)
1.140
1.141 text{* Instantiation for intervals on @{text ordered_euclidean_space} *}
1.142
1.143 @@ -5295,14 +5298,14 @@
1.144 shows "closed {.. a}"
1.145 unfolding eucl_atMost_eq_halfspaces
1.146 by (intro closed_INT ballI closed_Collect_le
1.147 - continuous_at_euclidean_component continuous_const)
1.148 + euclidean_component.isCont isCont_const)
1.149
1.150 lemma closed_eucl_atLeast[simp, intro]:
1.151 fixes a :: "'a\<Colon>ordered_euclidean_space"
1.152 shows "closed {a ..}"
1.153 unfolding eucl_atLeast_eq_halfspaces
1.154 by (intro closed_INT ballI closed_Collect_le
1.155 - continuous_at_euclidean_component continuous_const)
1.156 + euclidean_component.isCont isCont_const)
1.157
1.158 lemma open_vimage_euclidean_component: "open S \<Longrightarrow> open ((\<lambda>x. x $$ i) -` S)"
1.159 by (auto intro!: continuous_open_vimage)