add lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq;
simplify and generalize some proofs;
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Mon Aug 15 12:18:34 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Mon Aug 15 14:09:39 2011 -0700
@@ -1093,34 +1093,21 @@
done
qed
+lemma continuous_at_component: "continuous (at a) (\<lambda>x. x $ i)"
+unfolding continuous_at by (intro tendsto_intros)
+
+lemma continuous_on_component: "continuous_on s (\<lambda>x. x $ i)"
+unfolding continuous_on_def by (intro ballI tendsto_intros)
+
lemma closed_positive_orthant: "closed {x::real^'n. \<forall>i. 0 \<le>x$i}"
-proof-
- let ?U = "UNIV :: 'n set"
- let ?O = "{x::real^'n. \<forall>i. x$i\<ge>0}"
- {fix x:: "real^'n" and i::'n assume H: "\<forall>e>0. \<exists>x'\<in>?O. x' \<noteq> x \<and> dist x' x < e"
- and xi: "x$i < 0"
- from xi have th0: "-x$i > 0" by arith
- from H[rule_format, OF th0] obtain x' where x': "x' \<in>?O" "x' \<noteq> x" "dist x' x < -x $ i" by blast
- have th:" \<And>b a (x::real). abs x <= b \<Longrightarrow> b <= a ==> ~(a + x < 0)" by arith
- have th': "\<And>x (y::real). x < 0 \<Longrightarrow> 0 <= y ==> abs x <= abs (y - x)" by arith
- have th1: "\<bar>x$i\<bar> \<le> \<bar>(x' - x)$i\<bar>" using x'(1) xi
- apply (simp only: vector_component)
- by (rule th') auto
- have th2: "\<bar>dist x x'\<bar> \<ge> \<bar>(x' - x)$i\<bar>" using component_le_norm_cart[of "x'-x" i]
- apply (simp add: dist_norm) by norm
- from th[OF th1 th2] x'(3) have False by (simp add: dist_commute) }
- then show ?thesis unfolding closed_limpt islimpt_approachable
- unfolding not_le[symmetric] by blast
-qed
+ unfolding Collect_all_eq
+ by (intro closed_INT ballI closed_Collect_le continuous_const
+ continuous_at_component)
+
lemma Lim_component_cart:
fixes f :: "'a \<Rightarrow> 'b::metric_space ^ 'n"
shows "(f ---> l) net \<Longrightarrow> ((\<lambda>a. f a $i) ---> l$i) net"
- unfolding tendsto_iff
- apply (clarify)
- apply (drule spec, drule (1) mp)
- apply (erule eventually_elim1)
- apply (erule le_less_trans [OF dist_vec_nth_le])
- done
+ by (intro tendsto_intros)
lemma bounded_component_cart: "bounded s \<Longrightarrow> bounded ((\<lambda>x. x $ i) ` s)"
unfolding bounded_def
@@ -1193,12 +1180,6 @@
with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially" by auto
qed
-lemma continuous_at_component: "continuous (at a) (\<lambda>x. x $ i)"
-unfolding continuous_at by (intro tendsto_intros)
-
-lemma continuous_on_component: "continuous_on s (\<lambda>x. x $ i)"
-unfolding continuous_on_def by (intro ballI tendsto_intros)
-
lemma interval_cart: fixes a :: "'a::ord^'n" shows
"{a <..< b} = {x::'a^'n. \<forall>i. a$i < x$i \<and> x$i < b$i}" and
"{a .. b} = {x::'a^'n. \<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i}"
@@ -1307,27 +1288,15 @@
lemma closed_interval_left_cart: fixes b::"real^'n"
shows "closed {x::real^'n. \<forall>i. x$i \<le> b$i}"
-proof-
- { fix i
- fix x::"real^'n" assume x:"\<forall>e>0. \<exists>x'\<in>{x. \<forall>i. x $ i \<le> b $ i}. x' \<noteq> x \<and> dist x' x < e"
- { assume "x$i > b$i"
- then obtain y where "y $ i \<le> b $ i" "y \<noteq> x" "dist y x < x$i - b$i" using x[THEN spec[where x="x$i - b$i"]] by auto
- hence False using component_le_norm_cart[of "y - x" i] unfolding dist_norm and vector_minus_component by auto }
- hence "x$i \<le> b$i" by(rule ccontr)auto }
- thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
-qed
+ unfolding Collect_all_eq
+ by (intro closed_INT ballI closed_Collect_le continuous_const
+ continuous_at_component)
lemma closed_interval_right_cart: fixes a::"real^'n"
shows "closed {x::real^'n. \<forall>i. a$i \<le> x$i}"
-proof-
- { fix i
- fix x::"real^'n" assume x:"\<forall>e>0. \<exists>x'\<in>{x. \<forall>i. a $ i \<le> x $ i}. x' \<noteq> x \<and> dist x' x < e"
- { assume "a$i > x$i"
- then obtain y where "a $ i \<le> y $ i" "y \<noteq> x" "dist y x < a$i - x$i" using x[THEN spec[where x="a$i - x$i"]] by auto
- hence False using component_le_norm_cart[of "y - x" i] unfolding dist_norm and vector_minus_component by auto }
- hence "a$i \<le> x$i" by(rule ccontr)auto }
- thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
-qed
+ unfolding Collect_all_eq
+ by (intro closed_INT ballI closed_Collect_le continuous_const
+ continuous_at_component)
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)"
@@ -1335,19 +1304,19 @@
lemma closed_halfspace_component_le_cart:
shows "closed {x::real^'n. x$i \<le> a}"
- using closed_halfspace_le[of "(cart_basis i)::real^'n" a] unfolding inner_basis[OF assms] by auto
+ by (intro closed_Collect_le continuous_at_component continuous_const)
lemma closed_halfspace_component_ge_cart:
shows "closed {x::real^'n. x$i \<ge> a}"
- using closed_halfspace_ge[of a "(cart_basis i)::real^'n"] unfolding inner_basis[OF assms] by auto
+ by (intro closed_Collect_le continuous_at_component continuous_const)
lemma open_halfspace_component_lt_cart:
shows "open {x::real^'n. x$i < a}"
- using open_halfspace_lt[of "(cart_basis i)::real^'n" a] unfolding inner_basis[OF assms] by auto
+ by (intro open_Collect_less continuous_at_component continuous_const)
lemma open_halfspace_component_gt_cart:
shows "open {x::real^'n. x$i > a}"
- using open_halfspace_gt[of a "(cart_basis i)::real^'n"] unfolding inner_basis[OF assms] by auto
+ by (intro open_Collect_less continuous_at_component continuous_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"
@@ -1382,23 +1351,14 @@
unfolding subspace_def by auto
lemma closed_substandard_cart:
- "closed {x::real^'n. \<forall>i. P i --> x$i = 0}" (is "closed ?A")
+ "closed {x::'a::real_normed_vector ^ 'n. \<forall>i. P i \<longrightarrow> x$i = 0}"
proof-
- let ?D = "{i. P i}"
- let ?Bs = "{{x::real^'n. inner (cart_basis i) x = 0}| i. i \<in> ?D}"
- { fix x
- { assume "x\<in>?A"
- hence x:"\<forall>i\<in>?D. x $ i = 0" by auto
- hence "x\<in> \<Inter> ?Bs" by(auto simp add: inner_basis x) }
- moreover
- { assume x:"x\<in>\<Inter>?Bs"
- { fix i assume i:"i \<in> ?D"
- then obtain B where BB:"B \<in> ?Bs" and B:"B = {x::real^'n. inner (cart_basis i) x = 0}" by auto
- hence "x $ i = 0" unfolding B using x unfolding inner_basis by auto }
- hence "x\<in>?A" by auto }
- ultimately have "x\<in>?A \<longleftrightarrow> x\<in> \<Inter>?Bs" .. }
- hence "?A = \<Inter> ?Bs" by auto
- thus ?thesis by(auto simp add: closed_Inter closed_hyperplane)
+ { 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) }
+ thus ?thesis
+ unfolding Collect_all_eq by (simp add: closed_INT)
qed
lemma dim_substandard_cart:
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Aug 15 12:18:34 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Aug 15 14:09:39 2011 -0700
@@ -5152,6 +5152,52 @@
subsection {* Closure of halfspaces and hyperplanes *}
+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"
+ 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])
+ 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"
+ 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])
+ also have "((\<lambda>x. g x - f x) -` {0..}) = {x. f x \<le> g x}"
+ by auto
+ finally show ?thesis .
+qed
+
+lemma closed_Collect_eq:
+ fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
+ (* FIXME: generalize 'a to topological_space *)
+ (* FIXME: generalize 'b to t2_space *)
+ assumes f: "\<And>x. continuous (at x) f"
+ assumes g: "\<And>x. continuous (at x) g"
+ shows "closed {x. f x = g x}"
+proof -
+ have "closed ((\<lambda>x. g x - f x) -` {0})"
+ using continuous_sub [OF g f] closed_singleton
+ by (rule continuous_closed_vimage [rule_format])
+ also have "((\<lambda>x. g x - f x) -` {0}) = {x. f x = g x}"
+ by auto
+ finally show ?thesis .
+qed
+
lemma Lim_inner:
assumes "(f ---> l) net" shows "((\<lambda>y. inner a (f y)) ---> inner a l) net"
by (intro tendsto_intros assms)
@@ -5168,53 +5214,41 @@
unfolding continuous_on by (rule ballI) (intro tendsto_intros)
lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
-proof-
- have "\<forall>x. continuous (at x) (inner a)"
- unfolding continuous_at by (rule allI) (intro tendsto_intros)
- hence "closed (inner a -` {..b})"
- using closed_real_atMost by (rule continuous_closed_vimage)
- moreover have "{x. inner a x \<le> b} = inner a -` {..b}" by auto
- ultimately show ?thesis by simp
-qed
+ by (intro closed_Collect_le continuous_at_inner continuous_const)
lemma closed_halfspace_ge: "closed {x. inner a x \<ge> b}"
- using closed_halfspace_le[of "-a" "-b"] unfolding inner_minus_left by auto
+ by (intro closed_Collect_le continuous_at_inner continuous_const)
lemma closed_hyperplane: "closed {x. inner a x = b}"
-proof-
- have "{x. inner a x = b} = {x. inner a x \<ge> b} \<inter> {x. inner a x \<le> b}" by auto
- thus ?thesis using closed_halfspace_le[of a b] and closed_halfspace_ge[of b a] using closed_Int by auto
-qed
+ by (intro closed_Collect_eq continuous_at_inner continuous_const)
lemma closed_halfspace_component_le:
shows "closed {x::'a::euclidean_space. x$$i \<le> a}"
- using closed_halfspace_le[of "(basis i)::'a" a] unfolding euclidean_component_def .
+ by (intro closed_Collect_le continuous_at_euclidean_component
+ continuous_const)
lemma closed_halfspace_component_ge:
shows "closed {x::'a::euclidean_space. x$$i \<ge> a}"
- using closed_halfspace_ge[of a "(basis i)::'a"] unfolding euclidean_component_def .
+ by (intro closed_Collect_le continuous_at_euclidean_component
+ continuous_const)
text {* Openness of halfspaces. *}
lemma open_halfspace_lt: "open {x. inner a x < b}"
-proof-
- have "- {x. b \<le> inner a x} = {x. inner a x < b}" by auto
- thus ?thesis using closed_halfspace_ge[unfolded closed_def, of b a] by auto
-qed
+ by (intro open_Collect_less continuous_at_inner continuous_const)
lemma open_halfspace_gt: "open {x. inner a x > b}"
-proof-
- have "- {x. b \<ge> inner a x} = {x. inner a x > b}" by auto
- thus ?thesis using closed_halfspace_le[unfolded closed_def, of a b] by auto
-qed
+ by (intro open_Collect_less continuous_at_inner continuous_const)
lemma open_halfspace_component_lt:
shows "open {x::'a::euclidean_space. x$$i < a}"
- using open_halfspace_lt[of "(basis i)::'a" a] unfolding euclidean_component_def .
+ by (intro open_Collect_less continuous_at_euclidean_component
+ continuous_const)
lemma open_halfspace_component_gt:
shows "open {x::'a::euclidean_space. x$$i > a}"
- using open_halfspace_gt[of a "(basis i)::'a"] unfolding euclidean_component_def .
+ by (intro open_Collect_less continuous_at_euclidean_component
+ continuous_const)
text{* Instantiation for intervals on @{text ordered_euclidean_space} *}
@@ -5252,23 +5286,15 @@
fixes a :: "'a\<Colon>ordered_euclidean_space"
shows "closed {.. a}"
unfolding eucl_atMost_eq_halfspaces
-proof (safe intro!: closed_INT)
- fix i :: nat
- have "- {x::'a. x $$ i \<le> a $$ i} = {x. a $$ i < x $$ i}" by auto
- then show "closed {x::'a. x $$ i \<le> a $$ i}"
- by (simp add: closed_def open_halfspace_component_gt)
-qed
+ by (intro closed_INT ballI closed_Collect_le
+ continuous_at_euclidean_component continuous_const)
lemma closed_eucl_atLeast[simp, intro]:
fixes a :: "'a\<Colon>ordered_euclidean_space"
shows "closed {a ..}"
unfolding eucl_atLeast_eq_halfspaces
-proof (safe intro!: closed_INT)
- fix i :: nat
- have "- {x::'a. a $$ i \<le> x $$ i} = {x. x $$ i < a $$ i}" by auto
- then show "closed {x::'a. a $$ i \<le> x $$ i}"
- by (simp add: closed_def open_halfspace_component_lt)
-qed
+ by (intro closed_INT ballI closed_Collect_le
+ continuous_at_euclidean_component continuous_const)
lemma open_vimage_euclidean_component: "open S \<Longrightarrow> open ((\<lambda>x. x $$ i) -` S)"
by (auto intro!: continuous_open_vimage)