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.5  subsection {* Closure of halfspaces and hyperplanes *}
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.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.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.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.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.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.93  text {* Openness of halfspaces. *}
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.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.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.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.121  text{* Instantiation for intervals on @{text ordered_euclidean_space} *}
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.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.149  lemma open_vimage_euclidean_component: "open S \<Longrightarrow> open ((\<lambda>x. x \$\$ i) -` S)"
1.150    by (auto intro!: continuous_open_vimage)