generalize lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq to class topological_space
authorhuffman
Mon Aug 15 18:35:36 2011 -0700 (2011-08-15)
changeset 44219f738e3200e24
parent 44218 f0e442e24816
child 44220 e5753e2a5944
generalize lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq to class topological_space
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon Aug 15 16:48:05 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon Aug 15 18:35:36 2011 -0700
     1.3 @@ -1101,8 +1101,7 @@
     1.4  
     1.5  lemma closed_positive_orthant: "closed {x::real^'n. \<forall>i. 0 \<le>x$i}"
     1.6    unfolding Collect_all_eq
     1.7 -  by (intro closed_INT ballI closed_Collect_le continuous_const
     1.8 -    continuous_at_component)
     1.9 +  by (intro closed_INT ballI closed_Collect_le isCont_const vec_nth.isCont)
    1.10  
    1.11  lemma Lim_component_cart:
    1.12    fixes f :: "'a \<Rightarrow> 'b::metric_space ^ 'n"
    1.13 @@ -1289,14 +1288,12 @@
    1.14  lemma closed_interval_left_cart: fixes b::"real^'n"
    1.15    shows "closed {x::real^'n. \<forall>i. x$i \<le> b$i}"
    1.16    unfolding Collect_all_eq
    1.17 -  by (intro closed_INT ballI closed_Collect_le continuous_const
    1.18 -    continuous_at_component)
    1.19 +  by (intro closed_INT ballI closed_Collect_le isCont_const vec_nth.isCont)
    1.20  
    1.21  lemma closed_interval_right_cart: fixes a::"real^'n"
    1.22    shows "closed {x::real^'n. \<forall>i. a$i \<le> x$i}"
    1.23    unfolding Collect_all_eq
    1.24 -  by (intro closed_INT ballI closed_Collect_le continuous_const
    1.25 -    continuous_at_component)
    1.26 +  by (intro closed_INT ballI closed_Collect_le isCont_const vec_nth.isCont)
    1.27  
    1.28  lemma is_interval_cart:"is_interval (s::(real^'n) set) \<longleftrightarrow>
    1.29    (\<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)"
    1.30 @@ -1304,19 +1301,19 @@
    1.31  
    1.32  lemma closed_halfspace_component_le_cart:
    1.33    shows "closed {x::real^'n. x$i \<le> a}"
    1.34 -  by (intro closed_Collect_le continuous_at_component continuous_const)
    1.35 +  by (intro closed_Collect_le vec_nth.isCont isCont_const)
    1.36  
    1.37  lemma closed_halfspace_component_ge_cart:
    1.38    shows "closed {x::real^'n. x$i \<ge> a}"
    1.39 -  by (intro closed_Collect_le continuous_at_component continuous_const)
    1.40 +  by (intro closed_Collect_le vec_nth.isCont isCont_const)
    1.41  
    1.42  lemma open_halfspace_component_lt_cart:
    1.43    shows "open {x::real^'n. x$i < a}"
    1.44 -  by (intro open_Collect_less continuous_at_component continuous_const)
    1.45 +  by (intro open_Collect_less vec_nth.isCont isCont_const)
    1.46  
    1.47  lemma open_halfspace_component_gt_cart:
    1.48    shows "open {x::real^'n. x$i  > a}"
    1.49 -  by (intro open_Collect_less continuous_at_component continuous_const)
    1.50 +  by (intro open_Collect_less vec_nth.isCont isCont_const)
    1.51  
    1.52  lemma Lim_component_le_cart: fixes f :: "'a \<Rightarrow> real^'n"
    1.53    assumes "(f ---> l) net" "\<not> (trivial_limit net)"  "eventually (\<lambda>x. f(x)$i \<le> b) net"
    1.54 @@ -1355,8 +1352,8 @@
    1.55  proof-
    1.56    { fix i::'n
    1.57      have "closed {x::'a ^ 'n. P i \<longrightarrow> x$i = 0}"
    1.58 -      by (cases "P i", simp_all, intro closed_Collect_eq
    1.59 -        continuous_at_component continuous_const) }
    1.60 +      by (cases "P i", simp_all,
    1.61 +        intro closed_Collect_eq vec_nth.isCont isCont_const) }
    1.62    thus ?thesis
    1.63      unfolding Collect_all_eq by (simp add: closed_INT)
    1.64  qed
     2.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 15 16:48:05 2011 -0700
     2.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 15 18:35:36 2011 -0700
     2.3 @@ -5152,56 +5152,63 @@
     2.4  
     2.5  subsection {* Closure of halfspaces and hyperplanes *}
     2.6  
     2.7 +lemma isCont_open_vimage:
     2.8 +  assumes "\<And>x. isCont f x" and "open s" shows "open (f -` s)"
     2.9 +proof -
    2.10 +  from assms(1) have "continuous_on UNIV f"
    2.11 +    unfolding isCont_def continuous_on_def within_UNIV by simp
    2.12 +  hence "open {x \<in> UNIV. f x \<in> s}"
    2.13 +    using open_UNIV `open s` by (rule continuous_open_preimage)
    2.14 +  thus "open (f -` s)"
    2.15 +    by (simp add: vimage_def)
    2.16 +qed
    2.17 +
    2.18 +lemma isCont_closed_vimage:
    2.19 +  assumes "\<And>x. isCont f x" and "closed s" shows "closed (f -` s)"
    2.20 +  using assms unfolding closed_def vimage_Compl [symmetric]
    2.21 +  by (rule isCont_open_vimage)
    2.22 +
    2.23  lemma open_Collect_less:
    2.24 -  fixes f g :: "'a::t2_space \<Rightarrow> real"
    2.25 -  (* FIXME: generalize to topological_space *)
    2.26 -  assumes f: "\<And>x. continuous (at x) f"
    2.27 -  assumes g: "\<And>x. continuous (at x) g"
    2.28 +  fixes f g :: "'a::topological_space \<Rightarrow> real"
    2.29 +  assumes f: "\<And>x. isCont f x"
    2.30 +  assumes g: "\<And>x. isCont g x"
    2.31    shows "open {x. f x < g x}"
    2.32  proof -
    2.33    have "open ((\<lambda>x. g x - f x) -` {0<..})"
    2.34 -    using continuous_sub [OF g f] open_real_greaterThan
    2.35 -    by (rule continuous_open_vimage [rule_format])
    2.36 +    using isCont_diff [OF g f] open_real_greaterThan
    2.37 +    by (rule isCont_open_vimage)
    2.38    also have "((\<lambda>x. g x - f x) -` {0<..}) = {x. f x < g x}"
    2.39      by auto
    2.40    finally show ?thesis .
    2.41  qed
    2.42  
    2.43  lemma closed_Collect_le:
    2.44 -  fixes f g :: "'a::t2_space \<Rightarrow> real"
    2.45 -  (* FIXME: generalize to topological_space *)
    2.46 -  assumes f: "\<And>x. continuous (at x) f"
    2.47 -  assumes g: "\<And>x. continuous (at x) g"
    2.48 +  fixes f g :: "'a::topological_space \<Rightarrow> real"
    2.49 +  assumes f: "\<And>x. isCont f x"
    2.50 +  assumes g: "\<And>x. isCont g x"
    2.51    shows "closed {x. f x \<le> g x}"
    2.52  proof -
    2.53    have "closed ((\<lambda>x. g x - f x) -` {0..})"
    2.54 -    using continuous_sub [OF g f] closed_real_atLeast
    2.55 -    by (rule continuous_closed_vimage [rule_format])
    2.56 +    using isCont_diff [OF g f] closed_real_atLeast
    2.57 +    by (rule isCont_closed_vimage)
    2.58    also have "((\<lambda>x. g x - f x) -` {0..}) = {x. f x \<le> g x}"
    2.59      by auto
    2.60    finally show ?thesis .
    2.61  qed
    2.62  
    2.63 -lemma continuous_at_Pair: (* TODO: move *)
    2.64 -  assumes f: "continuous (at x) f"
    2.65 -  assumes g: "continuous (at x) g"
    2.66 -  shows "continuous (at x) (\<lambda>x. (f x, g x))"
    2.67 -  using assms unfolding continuous_at by (rule tendsto_Pair)
    2.68 -
    2.69  lemma closed_Collect_eq:
    2.70 -  fixes f g :: "'a::t2_space \<Rightarrow> 'b::t2_space"
    2.71 -  (* FIXME: generalize 'a to topological_space *)
    2.72 -  assumes f: "\<And>x. continuous (at x) f"
    2.73 -  assumes g: "\<And>x. continuous (at x) g"
    2.74 +  fixes f g :: "'a::topological_space \<Rightarrow> 'b::t2_space"
    2.75 +  assumes f: "\<And>x. isCont f x"
    2.76 +  assumes g: "\<And>x. isCont g x"
    2.77    shows "closed {x. f x = g x}"
    2.78  proof -
    2.79    have "open {(x::'b, y::'b). x \<noteq> y}"
    2.80      unfolding open_prod_def by (auto dest!: hausdorff)
    2.81    hence "closed {(x::'b, y::'b). x = y}"
    2.82      unfolding closed_def split_def Collect_neg_eq .
    2.83 -  with continuous_at_Pair [OF f g]
    2.84 +  with isCont_Pair [OF f g]
    2.85    have "closed ((\<lambda>x. (f x, g x)) -` {(x, y). x = y})"
    2.86 -    by (rule continuous_closed_vimage [rule_format])
    2.87 +    by (rule isCont_closed_vimage)
    2.88    also have "\<dots> = {x. f x = g x}" by auto
    2.89    finally show ?thesis .
    2.90  qed
    2.91 @@ -5222,41 +5229,37 @@
    2.92    unfolding continuous_on by (rule ballI) (intro tendsto_intros)
    2.93  
    2.94  lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
    2.95 -  by (intro closed_Collect_le continuous_at_inner continuous_const)
    2.96 +  by (intro closed_Collect_le inner.isCont isCont_const isCont_ident)
    2.97  
    2.98  lemma closed_halfspace_ge: "closed {x. inner a x \<ge> b}"
    2.99 -  by (intro closed_Collect_le continuous_at_inner continuous_const)
   2.100 +  by (intro closed_Collect_le inner.isCont isCont_const isCont_ident)
   2.101  
   2.102  lemma closed_hyperplane: "closed {x. inner a x = b}"
   2.103 -  by (intro closed_Collect_eq continuous_at_inner continuous_const)
   2.104 +  by (intro closed_Collect_eq inner.isCont isCont_const isCont_ident)
   2.105  
   2.106  lemma closed_halfspace_component_le:
   2.107    shows "closed {x::'a::euclidean_space. x$$i \<le> a}"
   2.108 -  by (intro closed_Collect_le continuous_at_euclidean_component
   2.109 -    continuous_const)
   2.110 +  by (intro closed_Collect_le euclidean_component.isCont isCont_const)
   2.111  
   2.112  lemma closed_halfspace_component_ge:
   2.113    shows "closed {x::'a::euclidean_space. x$$i \<ge> a}"
   2.114 -  by (intro closed_Collect_le continuous_at_euclidean_component
   2.115 -    continuous_const)
   2.116 +  by (intro closed_Collect_le euclidean_component.isCont isCont_const)
   2.117  
   2.118  text {* Openness of halfspaces. *}
   2.119  
   2.120  lemma open_halfspace_lt: "open {x. inner a x < b}"
   2.121 -  by (intro open_Collect_less continuous_at_inner continuous_const)
   2.122 +  by (intro open_Collect_less inner.isCont isCont_const isCont_ident)
   2.123  
   2.124  lemma open_halfspace_gt: "open {x. inner a x > b}"
   2.125 -  by (intro open_Collect_less continuous_at_inner continuous_const)
   2.126 +  by (intro open_Collect_less inner.isCont isCont_const isCont_ident)
   2.127  
   2.128  lemma open_halfspace_component_lt:
   2.129    shows "open {x::'a::euclidean_space. x$$i < a}"
   2.130 -  by (intro open_Collect_less continuous_at_euclidean_component
   2.131 -    continuous_const)
   2.132 +  by (intro open_Collect_less euclidean_component.isCont isCont_const)
   2.133  
   2.134  lemma open_halfspace_component_gt:
   2.135 -  shows "open {x::'a::euclidean_space. x$$i  > a}"
   2.136 -  by (intro open_Collect_less continuous_at_euclidean_component
   2.137 -    continuous_const)
   2.138 +  shows "open {x::'a::euclidean_space. x$$i > a}"
   2.139 +  by (intro open_Collect_less euclidean_component.isCont isCont_const)
   2.140  
   2.141  text{* Instantiation for intervals on @{text ordered_euclidean_space} *}
   2.142  
   2.143 @@ -5295,14 +5298,14 @@
   2.144    shows "closed {.. a}"
   2.145    unfolding eucl_atMost_eq_halfspaces
   2.146    by (intro closed_INT ballI closed_Collect_le
   2.147 -    continuous_at_euclidean_component continuous_const)
   2.148 +    euclidean_component.isCont isCont_const)
   2.149  
   2.150  lemma closed_eucl_atLeast[simp, intro]:
   2.151    fixes a :: "'a\<Colon>ordered_euclidean_space"
   2.152    shows "closed {a ..}"
   2.153    unfolding eucl_atLeast_eq_halfspaces
   2.154    by (intro closed_INT ballI closed_Collect_le
   2.155 -    continuous_at_euclidean_component continuous_const)
   2.156 +    euclidean_component.isCont isCont_const)
   2.157  
   2.158  lemma open_vimage_euclidean_component: "open S \<Longrightarrow> open ((\<lambda>x. x $$ i) -` S)"
   2.159    by (auto intro!: continuous_open_vimage)