summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

generalize lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq to class topological_space

author | huffman |

Mon, 15 Aug 2011 18:35:36 -0700 | |

changeset 44219 | f738e3200e24 |

parent 44218 | f0e442e24816 |

child 44220 | e5753e2a5944 |

generalize lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq to class topological_space

--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Mon Aug 15 16:48:05 2011 -0700 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Mon Aug 15 18:35:36 2011 -0700 @@ -1101,8 +1101,7 @@ lemma closed_positive_orthant: "closed {x::real^'n. \<forall>i. 0 \<le>x$i}" unfolding Collect_all_eq - by (intro closed_INT ballI closed_Collect_le continuous_const - continuous_at_component) + by (intro closed_INT ballI closed_Collect_le isCont_const vec_nth.isCont) lemma Lim_component_cart: fixes f :: "'a \<Rightarrow> 'b::metric_space ^ 'n" @@ -1289,14 +1288,12 @@ lemma closed_interval_left_cart: fixes b::"real^'n" shows "closed {x::real^'n. \<forall>i. x$i \<le> b$i}" unfolding Collect_all_eq - by (intro closed_INT ballI closed_Collect_le continuous_const - continuous_at_component) + by (intro closed_INT ballI closed_Collect_le isCont_const vec_nth.isCont) lemma closed_interval_right_cart: fixes a::"real^'n" shows "closed {x::real^'n. \<forall>i. a$i \<le> x$i}" unfolding Collect_all_eq - by (intro closed_INT ballI closed_Collect_le continuous_const - continuous_at_component) + by (intro closed_INT ballI closed_Collect_le isCont_const vec_nth.isCont) lemma is_interval_cart:"is_interval (s::(real^'n) set) \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i. ((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)" @@ -1304,19 +1301,19 @@ lemma closed_halfspace_component_le_cart: shows "closed {x::real^'n. x$i \<le> a}" - by (intro closed_Collect_le continuous_at_component continuous_const) + by (intro closed_Collect_le vec_nth.isCont isCont_const) lemma closed_halfspace_component_ge_cart: shows "closed {x::real^'n. x$i \<ge> a}" - by (intro closed_Collect_le continuous_at_component continuous_const) + by (intro closed_Collect_le vec_nth.isCont isCont_const) lemma open_halfspace_component_lt_cart: shows "open {x::real^'n. x$i < a}" - by (intro open_Collect_less continuous_at_component continuous_const) + by (intro open_Collect_less vec_nth.isCont isCont_const) lemma open_halfspace_component_gt_cart: shows "open {x::real^'n. x$i > a}" - by (intro open_Collect_less continuous_at_component continuous_const) + by (intro open_Collect_less vec_nth.isCont isCont_const) lemma Lim_component_le_cart: fixes f :: "'a \<Rightarrow> real^'n" assumes "(f ---> l) net" "\<not> (trivial_limit net)" "eventually (\<lambda>x. f(x)$i \<le> b) net" @@ -1355,8 +1352,8 @@ proof- { fix i::'n have "closed {x::'a ^ 'n. P i \<longrightarrow> x$i = 0}" - by (cases "P i", simp_all, intro closed_Collect_eq - continuous_at_component continuous_const) } + by (cases "P i", simp_all, + intro closed_Collect_eq vec_nth.isCont isCont_const) } thus ?thesis unfolding Collect_all_eq by (simp add: closed_INT) qed

--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Aug 15 16:48:05 2011 -0700 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Aug 15 18:35:36 2011 -0700 @@ -5152,56 +5152,63 @@ subsection {* Closure of halfspaces and hyperplanes *} +lemma isCont_open_vimage: + assumes "\<And>x. isCont f x" and "open s" shows "open (f -` s)" +proof - + from assms(1) have "continuous_on UNIV f" + unfolding isCont_def continuous_on_def within_UNIV by simp + hence "open {x \<in> UNIV. f x \<in> s}" + using open_UNIV `open s` by (rule continuous_open_preimage) + thus "open (f -` s)" + by (simp add: vimage_def) +qed + +lemma isCont_closed_vimage: + assumes "\<And>x. isCont f x" and "closed s" shows "closed (f -` s)" + using assms unfolding closed_def vimage_Compl [symmetric] + by (rule isCont_open_vimage) + lemma open_Collect_less: - fixes f g :: "'a::t2_space \<Rightarrow> real" - (* FIXME: generalize to topological_space *) - assumes f: "\<And>x. continuous (at x) f" - assumes g: "\<And>x. continuous (at x) g" + fixes f g :: "'a::topological_space \<Rightarrow> real" + assumes f: "\<And>x. isCont f x" + assumes g: "\<And>x. isCont g x" shows "open {x. f x < g x}" proof - have "open ((\<lambda>x. g x - f x) -` {0<..})" - using continuous_sub [OF g f] open_real_greaterThan - by (rule continuous_open_vimage [rule_format]) + using isCont_diff [OF g f] open_real_greaterThan + by (rule isCont_open_vimage) also have "((\<lambda>x. g x - f x) -` {0<..}) = {x. f x < g x}" by auto finally show ?thesis . qed lemma closed_Collect_le: - fixes f g :: "'a::t2_space \<Rightarrow> real" - (* FIXME: generalize to topological_space *) - assumes f: "\<And>x. continuous (at x) f" - assumes g: "\<And>x. continuous (at x) g" + fixes f g :: "'a::topological_space \<Rightarrow> real" + assumes f: "\<And>x. isCont f x" + assumes g: "\<And>x. isCont g x" shows "closed {x. f x \<le> g x}" proof - have "closed ((\<lambda>x. g x - f x) -` {0..})" - using continuous_sub [OF g f] closed_real_atLeast - by (rule continuous_closed_vimage [rule_format]) + using isCont_diff [OF g f] closed_real_atLeast + by (rule isCont_closed_vimage) also have "((\<lambda>x. g x - f x) -` {0..}) = {x. f x \<le> g x}" by auto finally show ?thesis . qed -lemma continuous_at_Pair: (* TODO: move *) - assumes f: "continuous (at x) f" - assumes g: "continuous (at x) g" - shows "continuous (at x) (\<lambda>x. (f x, g x))" - using assms unfolding continuous_at by (rule tendsto_Pair) - lemma closed_Collect_eq: - fixes f g :: "'a::t2_space \<Rightarrow> 'b::t2_space" - (* FIXME: generalize 'a to topological_space *) - assumes f: "\<And>x. continuous (at x) f" - assumes g: "\<And>x. continuous (at x) g" + fixes f g :: "'a::topological_space \<Rightarrow> 'b::t2_space" + assumes f: "\<And>x. isCont f x" + assumes g: "\<And>x. isCont g x" shows "closed {x. f x = g x}" proof - have "open {(x::'b, y::'b). x \<noteq> y}" unfolding open_prod_def by (auto dest!: hausdorff) hence "closed {(x::'b, y::'b). x = y}" unfolding closed_def split_def Collect_neg_eq . - with continuous_at_Pair [OF f g] + with isCont_Pair [OF f g] have "closed ((\<lambda>x. (f x, g x)) -` {(x, y). x = y})" - by (rule continuous_closed_vimage [rule_format]) + by (rule isCont_closed_vimage) also have "\<dots> = {x. f x = g x}" by auto finally show ?thesis . qed @@ -5222,41 +5229,37 @@ unfolding continuous_on by (rule ballI) (intro tendsto_intros) lemma closed_halfspace_le: "closed {x. inner a x \<le> b}" - by (intro closed_Collect_le continuous_at_inner continuous_const) + by (intro closed_Collect_le inner.isCont isCont_const isCont_ident) lemma closed_halfspace_ge: "closed {x. inner a x \<ge> b}" - by (intro closed_Collect_le continuous_at_inner continuous_const) + by (intro closed_Collect_le inner.isCont isCont_const isCont_ident) lemma closed_hyperplane: "closed {x. inner a x = b}" - by (intro closed_Collect_eq continuous_at_inner continuous_const) + by (intro closed_Collect_eq inner.isCont isCont_const isCont_ident) lemma closed_halfspace_component_le: shows "closed {x::'a::euclidean_space. x$$i \<le> a}" - by (intro closed_Collect_le continuous_at_euclidean_component - continuous_const) + by (intro closed_Collect_le euclidean_component.isCont isCont_const) lemma closed_halfspace_component_ge: shows "closed {x::'a::euclidean_space. x$$i \<ge> a}" - by (intro closed_Collect_le continuous_at_euclidean_component - continuous_const) + by (intro closed_Collect_le euclidean_component.isCont isCont_const) text {* Openness of halfspaces. *} lemma open_halfspace_lt: "open {x. inner a x < b}" - by (intro open_Collect_less continuous_at_inner continuous_const) + by (intro open_Collect_less inner.isCont isCont_const isCont_ident) lemma open_halfspace_gt: "open {x. inner a x > b}" - by (intro open_Collect_less continuous_at_inner continuous_const) + by (intro open_Collect_less inner.isCont isCont_const isCont_ident) lemma open_halfspace_component_lt: shows "open {x::'a::euclidean_space. x$$i < a}" - by (intro open_Collect_less continuous_at_euclidean_component - continuous_const) + by (intro open_Collect_less euclidean_component.isCont isCont_const) lemma open_halfspace_component_gt: - shows "open {x::'a::euclidean_space. x$$i > a}" - by (intro open_Collect_less continuous_at_euclidean_component - continuous_const) + shows "open {x::'a::euclidean_space. x$$i > a}" + by (intro open_Collect_less euclidean_component.isCont isCont_const) text{* Instantiation for intervals on @{text ordered_euclidean_space} *} @@ -5295,14 +5298,14 @@ shows "closed {.. a}" unfolding eucl_atMost_eq_halfspaces by (intro closed_INT ballI closed_Collect_le - continuous_at_euclidean_component continuous_const) + euclidean_component.isCont isCont_const) lemma closed_eucl_atLeast[simp, intro]: fixes a :: "'a\<Colon>ordered_euclidean_space" shows "closed {a ..}" unfolding eucl_atLeast_eq_halfspaces by (intro closed_INT ballI closed_Collect_le - continuous_at_euclidean_component continuous_const) + euclidean_component.isCont isCont_const) lemma open_vimage_euclidean_component: "open S \<Longrightarrow> open ((\<lambda>x. x $$ i) -` S)" by (auto intro!: continuous_open_vimage)