src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 44213 6fb54701a11b
parent 44212 4d10e7f342b1
child 44216 903bfe95fece
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 15 12:18:34 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 15 14:09:39 2011 -0700
     1.3 @@ -5152,6 +5152,52 @@
     1.4  
     1.5  subsection {* Closure of halfspaces and hyperplanes *}
     1.6  
     1.7 +lemma open_Collect_less:
     1.8 +  fixes f g :: "'a::t2_space \<Rightarrow> real"
     1.9 +  (* FIXME: generalize to topological_space *)
    1.10 +  assumes f: "\<And>x. continuous (at x) f"
    1.11 +  assumes g: "\<And>x. continuous (at x) g"
    1.12 +  shows "open {x. f x < g x}"
    1.13 +proof -
    1.14 +  have "open ((\<lambda>x. g x - f x) -` {0<..})"
    1.15 +    using continuous_sub [OF g f] open_real_greaterThan
    1.16 +    by (rule continuous_open_vimage [rule_format])
    1.17 +  also have "((\<lambda>x. g x - f x) -` {0<..}) = {x. f x < g x}"
    1.18 +    by auto
    1.19 +  finally show ?thesis .
    1.20 +qed
    1.21 +
    1.22 +lemma closed_Collect_le:
    1.23 +  fixes f g :: "'a::t2_space \<Rightarrow> real"
    1.24 +  (* FIXME: generalize to topological_space *)
    1.25 +  assumes f: "\<And>x. continuous (at x) f"
    1.26 +  assumes g: "\<And>x. continuous (at x) g"
    1.27 +  shows "closed {x. f x \<le> g x}"
    1.28 +proof -
    1.29 +  have "closed ((\<lambda>x. g x - f x) -` {0..})"
    1.30 +    using continuous_sub [OF g f] closed_real_atLeast
    1.31 +    by (rule continuous_closed_vimage [rule_format])
    1.32 +  also have "((\<lambda>x. g x - f x) -` {0..}) = {x. f x \<le> g x}"
    1.33 +    by auto
    1.34 +  finally show ?thesis .
    1.35 +qed
    1.36 +
    1.37 +lemma closed_Collect_eq:
    1.38 +  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
    1.39 +  (* FIXME: generalize 'a to topological_space *)
    1.40 +  (* FIXME: generalize 'b to t2_space *)
    1.41 +  assumes f: "\<And>x. continuous (at x) f"
    1.42 +  assumes g: "\<And>x. continuous (at x) g"
    1.43 +  shows "closed {x. f x = g x}"
    1.44 +proof -
    1.45 +  have "closed ((\<lambda>x. g x - f x) -` {0})"
    1.46 +    using continuous_sub [OF g f] closed_singleton
    1.47 +    by (rule continuous_closed_vimage [rule_format])
    1.48 +  also have "((\<lambda>x. g x - f x) -` {0}) = {x. f x = g x}"
    1.49 +    by auto
    1.50 +  finally show ?thesis .
    1.51 +qed
    1.52 +
    1.53  lemma Lim_inner:
    1.54    assumes "(f ---> l) net"  shows "((\<lambda>y. inner a (f y)) ---> inner a l) net"
    1.55    by (intro tendsto_intros assms)
    1.56 @@ -5168,53 +5214,41 @@
    1.57    unfolding continuous_on by (rule ballI) (intro tendsto_intros)
    1.58  
    1.59  lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
    1.60 -proof-
    1.61 -  have "\<forall>x. continuous (at x) (inner a)"
    1.62 -    unfolding continuous_at by (rule allI) (intro tendsto_intros)
    1.63 -  hence "closed (inner a -` {..b})"
    1.64 -    using closed_real_atMost by (rule continuous_closed_vimage)
    1.65 -  moreover have "{x. inner a x \<le> b} = inner a -` {..b}" by auto
    1.66 -  ultimately show ?thesis by simp
    1.67 -qed
    1.68 +  by (intro closed_Collect_le continuous_at_inner continuous_const)
    1.69  
    1.70  lemma closed_halfspace_ge: "closed {x. inner a x \<ge> b}"
    1.71 -  using closed_halfspace_le[of "-a" "-b"] unfolding inner_minus_left by auto
    1.72 +  by (intro closed_Collect_le continuous_at_inner continuous_const)
    1.73  
    1.74  lemma closed_hyperplane: "closed {x. inner a x = b}"
    1.75 -proof-
    1.76 -  have "{x. inner a x = b} = {x. inner a x \<ge> b} \<inter> {x. inner a x \<le> b}" by auto
    1.77 -  thus ?thesis using closed_halfspace_le[of a b] and closed_halfspace_ge[of b a] using closed_Int by auto
    1.78 -qed
    1.79 +  by (intro closed_Collect_eq continuous_at_inner continuous_const)
    1.80  
    1.81  lemma closed_halfspace_component_le:
    1.82    shows "closed {x::'a::euclidean_space. x$$i \<le> a}"
    1.83 -  using closed_halfspace_le[of "(basis i)::'a" a] unfolding euclidean_component_def .
    1.84 +  by (intro closed_Collect_le continuous_at_euclidean_component
    1.85 +    continuous_const)
    1.86  
    1.87  lemma closed_halfspace_component_ge:
    1.88    shows "closed {x::'a::euclidean_space. x$$i \<ge> a}"
    1.89 -  using closed_halfspace_ge[of a "(basis i)::'a"] unfolding euclidean_component_def .
    1.90 +  by (intro closed_Collect_le continuous_at_euclidean_component
    1.91 +    continuous_const)
    1.92  
    1.93  text {* Openness of halfspaces. *}
    1.94  
    1.95  lemma open_halfspace_lt: "open {x. inner a x < b}"
    1.96 -proof-
    1.97 -  have "- {x. b \<le> inner a x} = {x. inner a x < b}" by auto
    1.98 -  thus ?thesis using closed_halfspace_ge[unfolded closed_def, of b a] by auto
    1.99 -qed
   1.100 +  by (intro open_Collect_less continuous_at_inner continuous_const)
   1.101  
   1.102  lemma open_halfspace_gt: "open {x. inner a x > b}"
   1.103 -proof-
   1.104 -  have "- {x. b \<ge> inner a x} = {x. inner a x > b}" by auto
   1.105 -  thus ?thesis using closed_halfspace_le[unfolded closed_def, of a b] by auto
   1.106 -qed
   1.107 +  by (intro open_Collect_less continuous_at_inner continuous_const)
   1.108  
   1.109  lemma open_halfspace_component_lt:
   1.110    shows "open {x::'a::euclidean_space. x$$i < a}"
   1.111 -  using open_halfspace_lt[of "(basis i)::'a" a] unfolding euclidean_component_def .
   1.112 +  by (intro open_Collect_less continuous_at_euclidean_component
   1.113 +    continuous_const)
   1.114  
   1.115  lemma open_halfspace_component_gt:
   1.116    shows "open {x::'a::euclidean_space. x$$i  > a}"
   1.117 -  using open_halfspace_gt[of a "(basis i)::'a"] unfolding euclidean_component_def .
   1.118 +  by (intro open_Collect_less continuous_at_euclidean_component
   1.119 +    continuous_const)
   1.120  
   1.121  text{* Instantiation for intervals on @{text ordered_euclidean_space} *}
   1.122  
   1.123 @@ -5252,23 +5286,15 @@
   1.124    fixes a :: "'a\<Colon>ordered_euclidean_space"
   1.125    shows "closed {.. a}"
   1.126    unfolding eucl_atMost_eq_halfspaces
   1.127 -proof (safe intro!: closed_INT)
   1.128 -  fix i :: nat
   1.129 -  have "- {x::'a. x $$ i \<le> a $$ i} = {x. a $$ i < x $$ i}" by auto
   1.130 -  then show "closed {x::'a. x $$ i \<le> a $$ i}"
   1.131 -    by (simp add: closed_def open_halfspace_component_gt)
   1.132 -qed
   1.133 +  by (intro closed_INT ballI closed_Collect_le
   1.134 +    continuous_at_euclidean_component continuous_const)
   1.135  
   1.136  lemma closed_eucl_atLeast[simp, intro]:
   1.137    fixes a :: "'a\<Colon>ordered_euclidean_space"
   1.138    shows "closed {a ..}"
   1.139    unfolding eucl_atLeast_eq_halfspaces
   1.140 -proof (safe intro!: closed_INT)
   1.141 -  fix i :: nat
   1.142 -  have "- {x::'a. a $$ i \<le> x $$ i} = {x. x $$ i < a $$ i}" by auto
   1.143 -  then show "closed {x::'a. a $$ i \<le> x $$ i}"
   1.144 -    by (simp add: closed_def open_halfspace_component_lt)
   1.145 -qed
   1.146 +  by (intro closed_INT ballI closed_Collect_le
   1.147 +    continuous_at_euclidean_component continuous_const)
   1.148  
   1.149  lemma open_vimage_euclidean_component: "open S \<Longrightarrow> open ((\<lambda>x. x $$ i) -` S)"
   1.150    by (auto intro!: continuous_open_vimage)