author huffman Sat, 13 Jun 2009 13:10:10 -0700 changeset 31658 f5ffe064412a parent 31657 1dfa55a46d7d child 31659 937dea81dde0
generalize lemmas
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Sat Jun 13 11:56:41 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Sat Jun 13 13:10:10 2009 -0700
@@ -1238,7 +1238,7 @@

text{* Basic arithmetical combining theorems for limits. *}

-lemma Lim_linear: fixes f :: "('a \<Rightarrow> real^'n::finite)" and h :: "(real^'n \<Rightarrow> real^'m::finite)"
+lemma Lim_linear:
assumes "(f ---> l) net" "bounded_linear h"
shows "((\<lambda>x. h (f x)) ---> h l) net"
using `bounded_linear h` `(f ---> l) net`
@@ -1251,7 +1251,7 @@
by (rule tendsto_const)

lemma Lim_cmul:
-  fixes f :: "'a \<Rightarrow> real ^ 'n::finite"
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
shows "(f ---> l) net ==> ((\<lambda>x. c *\<^sub>R f x) ---> c *\<^sub>R l) net"
by (intro tendsto_intros)

@@ -1433,7 +1433,6 @@
text{* Limit under bilinear function *}

lemma Lim_bilinear:
-  fixes net :: "'a net" and h:: "real ^'m::finite \<Rightarrow> real ^'n::finite \<Rightarrow> real ^'p::finite"
assumes "(f ---> l) net" and "(g ---> m) net" and "bounded_bilinear h"
shows "((\<lambda>x. h (f x) (g x)) ---> (h l m)) net"
using `bounded_bilinear h` `(f ---> l) net` `(g ---> m) net`
@@ -2062,7 +2061,6 @@
qed

lemma bounded_linear_image:
-  fixes f :: "real^'m::finite \<Rightarrow> real^'n::finite"
assumes "bounded S" "bounded_linear f"
shows "bounded(f ` S)"
proof-
@@ -2078,7 +2076,7 @@
qed

lemma bounded_scaling:
-  fixes S :: "(real ^ 'n::finite) set"
+  fixes S :: "'a::real_normed_vector set"
shows "bounded S \<Longrightarrow> bounded ((\<lambda>x. c *\<^sub>R x) ` S)"
apply (rule bounded_linear_image, assumption)
apply (rule scaleR.bounded_linear_right)
@@ -3426,7 +3424,7 @@
by (auto simp add: continuous_def Lim_const)

lemma continuous_cmul:
-  fixes f :: "'a::t2_space \<Rightarrow> real ^ 'n::finite"
+  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
shows "continuous net f ==> continuous net (\<lambda>x. c *\<^sub>R f x)"
by (auto simp add: continuous_def Lim_cmul)

@@ -3452,7 +3450,7 @@
unfolding continuous_on_eq_continuous_within using continuous_const by blast

lemma continuous_on_cmul:
-  fixes f :: "'a::metric_space \<Rightarrow> real ^ _"
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
shows "continuous_on s f ==>  continuous_on s (\<lambda>x. c *\<^sub>R (f x))"
unfolding continuous_on_eq_continuous_within using continuous_cmul by blast

@@ -3480,7 +3478,8 @@
unfolding uniformly_continuous_on_def by simp

lemma uniformly_continuous_on_cmul:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> real ^ _"
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+    (* FIXME: generalize 'a to metric_space *)
assumes "uniformly_continuous_on s f"
shows "uniformly_continuous_on s (\<lambda>x. c *\<^sub>R f(x))"
proof-
@@ -3869,7 +3868,7 @@
qed

lemma open_affinity:
-  fixes s :: "(real ^ _) set"
+  fixes s :: "'a::real_normed_vector set"
assumes "open s"  "c \<noteq> 0"
shows "open ((\<lambda>x. a + c *\<^sub>R x) ` s)"
proof-
@@ -4021,7 +4020,7 @@

subsection{* Topological properties of linear functions.                               *}

-lemma linear_lim_0: fixes f::"real^'a::finite \<Rightarrow> real^'b::finite"
+lemma linear_lim_0:
assumes "bounded_linear f" shows "(f ---> 0) (at (0))"
proof-
interpret f: bounded_linear f by fact
@@ -4030,44 +4029,34 @@
thus ?thesis unfolding f.zero .
qed

-lemma bounded_linear_continuous_at:
+lemma linear_continuous_at:
assumes "bounded_linear f"  shows "continuous (at a) f"
unfolding continuous_at using assms
apply (rule bounded_linear.tendsto)
apply (rule tendsto_ident_at)
done

-lemma linear_continuous_at:
-  fixes f :: "real ^ _ \<Rightarrow> real ^ _"
-  assumes "bounded_linear f"  shows "continuous (at a) f"
-  using assms by (rule bounded_linear_continuous_at)
-
lemma linear_continuous_within:
-  fixes f :: "real ^ _ \<Rightarrow> real ^ _"
shows "bounded_linear f ==> continuous (at x within s) f"
using continuous_at_imp_continuous_within[of x f s] using linear_continuous_at[of f] by auto

lemma linear_continuous_on:
-  fixes f :: "real ^ _ \<Rightarrow> real ^ _"
shows "bounded_linear f ==> continuous_on s f"
using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto

text{* Also bilinear functions, in composition form.                             *}

lemma bilinear_continuous_at_compose:
-  fixes h :: "real ^ _ \<Rightarrow> real ^ _ \<Rightarrow> real ^ _"
shows "continuous (at x) f \<Longrightarrow> continuous (at x) g \<Longrightarrow> bounded_bilinear h
==> continuous (at x) (\<lambda>x. h (f x) (g x))"
unfolding continuous_at using Lim_bilinear[of f "f x" "(at x)" g "g x" h] by auto

lemma bilinear_continuous_within_compose:
-  fixes h :: "real ^ _ \<Rightarrow> real ^ _ \<Rightarrow> real ^ _"
shows "continuous (at x within s) f \<Longrightarrow> continuous (at x within s) g \<Longrightarrow> bounded_bilinear h
==> continuous (at x within s) (\<lambda>x. h (f x) (g x))"
unfolding continuous_within using Lim_bilinear[of f "f x"] by auto

lemma bilinear_continuous_on_compose:
-  fixes h :: "real ^ _ \<Rightarrow> real ^ _ \<Rightarrow> real ^ _"
shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> bounded_bilinear h
==> continuous_on s (\<lambda>x. h (f x) (g x))"
unfolding continuous_on_eq_continuous_within apply auto apply(erule_tac x=x in ballE) apply auto apply(erule_tac x=x in ballE) apply auto
@@ -4224,10 +4213,10 @@
subsection{* We can now extend limit compositions to consider the scalar multiplier.   *}

lemma Lim_mul:
-  fixes f :: "'a \<Rightarrow> real ^ _"
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
assumes "(c ---> d) net"  "(f ---> l) net"
shows "((\<lambda>x. c(x) *\<^sub>R f x) ---> (d *\<^sub>R l)) net"
-  unfolding smult_conv_scaleR using assms by (rule scaleR.tendsto)
+  using assms by (rule scaleR.tendsto)

lemma Lim_vmul:
fixes c :: "'a \<Rightarrow> real" and v :: "'b::real_normed_vector"
@@ -4358,25 +4347,20 @@

text{* Hence some useful properties follow quite easily.                         *}

-lemma compact_scaleR_image:
+lemma compact_scaling:
fixes s :: "'a::real_normed_vector set"
-  assumes "compact s"  shows "compact ((\<lambda>x. scaleR c x) ` s)"
+  assumes "compact s"  shows "compact ((\<lambda>x. c *\<^sub>R x) ` s)"
proof-
let ?f = "\<lambda>x. scaleR c x"
have *:"bounded_linear ?f" by (rule scaleR.bounded_linear_right)
show ?thesis using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f]
-    using bounded_linear_continuous_at[OF *] assms by auto
-qed
-
-lemma compact_scaling:
-  fixes s :: "(real ^ _) set"
-  assumes "compact s"  shows "compact ((\<lambda>x. c *\<^sub>R x) ` s)"
-  using assms unfolding smult_conv_scaleR by (rule compact_scaleR_image)
+    using linear_continuous_at[OF *] assms by auto
+qed

lemma compact_negations:
fixes s :: "'a::real_normed_vector set"
assumes "compact s"  shows "compact ((\<lambda>x. -x) ` s)"
-  using compact_scaleR_image [OF assms, of "- 1"] by auto
+  using compact_scaling [OF assms, of "- 1"] by auto

lemma compact_sums:
fixes s t :: "'a::real_normed_vector set"
@@ -4407,7 +4391,7 @@
qed

lemma compact_affinity:
-  fixes s :: "(real ^ _) set"
+  fixes s :: "'a::real_normed_vector set"
assumes "compact s"  shows "compact ((\<lambda>x. a + c *\<^sub>R x) ` s)"
proof-
have "op + a ` op *\<^sub>R c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s" by auto
@@ -4481,9 +4465,9 @@

text{* Related results with closure as the conclusion.                           *}

-lemma closed_scaleR_image:
+lemma closed_scaling:
fixes s :: "'a::real_normed_vector set"
-  assumes "closed s" shows "closed ((\<lambda>x. scaleR c x) ` s)"
+  assumes "closed s" shows "closed ((\<lambda>x. c *\<^sub>R x) ` s)"
proof(cases "s={}")
case True thus ?thesis by auto
next
@@ -4515,15 +4499,10 @@
qed
qed

-lemma closed_scaling:
-  fixes s :: "(real ^ _) set"
-  assumes "closed s" shows "closed ((\<lambda>x. c *\<^sub>R x) ` s)"
-  using assms unfolding smult_conv_scaleR by (rule closed_scaleR_image)
-
lemma closed_negations:
fixes s :: "'a::real_normed_vector set"
assumes "closed s"  shows "closed ((\<lambda>x. -x) ` s)"
-  using closed_scaleR_image[OF assms, of "- 1"] by simp
+  using closed_scaling[OF assms, of "- 1"] by simp

lemma compact_closed_sums:
fixes s :: "'a::real_normed_vector set"
@@ -5140,24 +5119,12 @@

subsection{* Closure of halfspaces and hyperplanes.                                    *}

-lemma Lim_dot: fixes f :: "real^'m \<Rightarrow> real^'n::finite"
-  assumes "(f ---> l) net"  shows "((\<lambda>y. a \<bullet> (f y)) ---> a \<bullet> l) net"
-  unfolding dot_def by (intro tendsto_intros assms)
-
-lemma continuous_at_dot:
-  fixes x :: "real ^ _"
-  shows "continuous (at x) (\<lambda>y. a \<bullet> y)"
-proof-
-  have "((\<lambda>x. x) ---> x) (at x)" unfolding Lim_at by auto
-  thus ?thesis unfolding continuous_at and o_def using Lim_dot[of "\<lambda>x. x" x "at x" a] by auto
-qed
-
-lemma continuous_on_dot:
-  fixes s :: "(real ^ _) set"
-  shows "continuous_on s (\<lambda>y. a \<bullet> y)"
-  using continuous_at_imp_continuous_on[of s "\<lambda>y. a \<bullet> y"]
-  using continuous_at_dot
-  by auto
+lemma Lim_inner:
+  assumes "(f ---> l) net"  shows "((\<lambda>y. inner a (f y)) ---> inner a l) net"
+  by (intro tendsto_intros assms)
+
+lemma continuous_at_inner: "continuous (at x) (inner a)"
+  unfolding continuous_at by (intro tendsto_intros)

lemma continuous_on_inner:
fixes s :: "'a::real_inner set"
@@ -5266,7 +5233,7 @@
using assms unfolding continuous_on unfolding Lim_within_union
unfolding Lim unfolding trivial_limit_within unfolding closed_limpt by auto

-lemma continuous_on_cases: fixes g :: "real^'m::finite \<Rightarrow> real ^'n::finite"
+lemma continuous_on_cases:
assumes "closed s" "closed t" "continuous_on s f" "continuous_on t g"
"\<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x"
shows "continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
@@ -5322,22 +5289,24 @@
(\<forall>x\<in>s. (g(f x) = x)) \<and> (f ` s = t) \<and> continuous_on s f \<and>
(\<forall>y\<in>t. (f(g y) = y)) \<and> (g ` t = s) \<and> continuous_on t g"

-definition homeomorphic :: "((real^'a::finite) set) \<Rightarrow> ((real^'b::finite) set) \<Rightarrow> bool" (infixr "homeomorphic" 60) where
+definition
+  homeomorphic :: "'a::metric_space set \<Rightarrow> 'b::metric_space set \<Rightarrow> bool"
+    (infixr "homeomorphic" 60) where
homeomorphic_def: "s homeomorphic t \<equiv> (\<exists>f g. homeomorphism s t f g)"

lemma homeomorphic_refl: "s homeomorphic s"
unfolding homeomorphic_def
unfolding homeomorphism_def
using continuous_on_id
-  apply(rule_tac x = "(\<lambda>x::real^'a.x)" in exI)
-  apply(rule_tac x = "(\<lambda>x::real^'b.x)" in exI)
+  apply(rule_tac x = "(\<lambda>x. x)" in exI)
+  apply(rule_tac x = "(\<lambda>x. x)" in exI)
by blast

lemma homeomorphic_sym:
"s homeomorphic t \<longleftrightarrow> t homeomorphic s"
unfolding homeomorphic_def
unfolding homeomorphism_def
-by blast
+by blast (* FIXME: slow *)

lemma homeomorphic_trans:
assumes "s homeomorphic t" "t homeomorphic u" shows "s homeomorphic u"
@@ -5379,7 +5348,8 @@
using assms unfolding inj_on_def inv_on_def by auto

lemma homeomorphism_compact:
-  fixes f :: "real ^ _ \<Rightarrow> real ^ _"
+  fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
+    (* class constraint due to continuous_on_inverse *)
assumes "compact s" "continuous_on s f"  "f ` s = t"  "inj_on f s"
shows "\<exists>g. homeomorphism s t f g"
proof-
@@ -5406,7 +5376,9 @@
qed

lemma homeomorphic_compact:
- "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s
+  fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
+    (* class constraint due to continuous_on_inverse *)
+  shows "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s
\<Longrightarrow> s homeomorphic t"
unfolding homeomorphic_def by(metis homeomorphism_compact)

@@ -5420,6 +5392,7 @@
text{* Results on translation, scaling etc.                                      *}

lemma homeomorphic_scaling:
+  fixes s :: "'a::real_normed_vector set"
assumes "c \<noteq> 0"  shows "s homeomorphic ((\<lambda>x. c *\<^sub>R x) ` s)"
unfolding homeomorphic_minimal
apply(rule_tac x="\<lambda>x. c *\<^sub>R x" in exI)
@@ -5428,13 +5401,15 @@
using continuous_on_cmul[OF continuous_on_id] by auto

lemma homeomorphic_translation:
- "s homeomorphic ((\<lambda>x. a + x) ` s)"
+  fixes s :: "'a::real_normed_vector set"
+  shows "s homeomorphic ((\<lambda>x. a + x) ` s)"
unfolding homeomorphic_minimal
apply(rule_tac x="\<lambda>x. a + x" in exI)
apply(rule_tac x="\<lambda>x. -a + x" in exI)
using continuous_on_add[OF continuous_on_const continuous_on_id] by auto

lemma homeomorphic_affinity:
+  fixes s :: "'a::real_normed_vector set"
assumes "c \<noteq> 0"  shows "s homeomorphic ((\<lambda>x. a + c *\<^sub>R x) ` s)"
proof-
have *:"op + a ` op *\<^sub>R c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s" by auto
@@ -5444,7 +5419,8 @@
using homeomorphic_translation[of "(\<lambda>x. c *\<^sub>R x) ` s" a] unfolding * by auto
qed

-lemma homeomorphic_balls: fixes a b ::"real^'a::finite"
+lemma homeomorphic_balls:
+  fixes a b ::"'a::real_normed_vector" (* FIXME: generalize to metric_space *)
assumes "0 < d"  "0 < e"
shows "(ball a d) homeomorphic  (ball b e)" (is ?th)
"(cball a d) homeomorphic (cball b e)" (is ?cth)