src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 changeset 44647 e4de7750cdeb parent 44632 076a45f65e12 child 44648 897f32a827f2
1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 01 07:31:33 2011 -0700
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 01 09:02:14 2011 -0700
1.3 @@ -3332,35 +3332,103 @@
1.5  text{* Combination results for pointwise continuity. *}
1.7 -lemma continuous_const: "continuous net (\<lambda>x. c)"
1.8 -  by (auto simp add: continuous_def tendsto_const)
1.9 -
1.10 -lemma continuous_cmul:
1.11 -  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
1.12 -  shows "continuous net f ==> continuous net (\<lambda>x. c *\<^sub>R f x)"
1.13 -  by (auto simp add: continuous_def intro: tendsto_intros)
1.14 -
1.15 -lemma continuous_neg:
1.16 -  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
1.17 -  shows "continuous net f ==> continuous net (\<lambda>x. -(f x))"
1.18 -  by (auto simp add: continuous_def tendsto_minus)
1.19 +lemma continuous_within_id: "continuous (at a within s) (\<lambda>x. x)"
1.20 +  unfolding continuous_within by (rule tendsto_ident_at_within)
1.21 +
1.22 +lemma continuous_at_id: "continuous (at a) (\<lambda>x. x)"
1.23 +  unfolding continuous_at by (rule tendsto_ident_at)
1.24 +
1.25 +lemma continuous_const: "continuous F (\<lambda>x. c)"
1.26 +  unfolding continuous_def by (rule tendsto_const)
1.27 +
1.28 +lemma continuous_dist:
1.29 +  assumes "continuous F f" and "continuous F g"
1.30 +  shows "continuous F (\<lambda>x. dist (f x) (g x))"
1.31 +  using assms unfolding continuous_def by (rule tendsto_dist)
1.32 +
1.33 +lemma continuous_norm:
1.34 +  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. norm (f x))"
1.35 +  unfolding continuous_def by (rule tendsto_norm)
1.36 +
1.37 +lemma continuous_infnorm:
1.38 +  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. infnorm (f x))"
1.39 +  unfolding continuous_def by (rule tendsto_infnorm)
1.42    fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
1.43 -  shows "continuous net f \<Longrightarrow> continuous net g \<Longrightarrow> continuous net (\<lambda>x. f x + g x)"
1.44 -  by (auto simp add: continuous_def tendsto_add)
1.45 -
1.46 -lemma continuous_sub:
1.47 +  shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x + g x)"
1.48 +  unfolding continuous_def by (rule tendsto_add)
1.49 +
1.50 +lemma continuous_minus:
1.51 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
1.52 +  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. - f x)"
1.53 +  unfolding continuous_def by (rule tendsto_minus)
1.54 +
1.55 +lemma continuous_diff:
1.56    fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
1.57 -  shows "continuous net f \<Longrightarrow> continuous net g \<Longrightarrow> continuous net (\<lambda>x. f x - g x)"
1.58 -  by (auto simp add: continuous_def tendsto_diff)
1.59 -
1.60 +  shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x - g x)"
1.61 +  unfolding continuous_def by (rule tendsto_diff)
1.62 +
1.63 +lemma continuous_scaleR:
1.64 +  fixes g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
1.65 +  shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x *\<^sub>R g x)"
1.66 +  unfolding continuous_def by (rule tendsto_scaleR)
1.67 +
1.68 +lemma continuous_mult:
1.69 +  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_algebra"
1.70 +  shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x * g x)"
1.71 +  unfolding continuous_def by (rule tendsto_mult)
1.72 +
1.73 +lemma continuous_inner:
1.74 +  assumes "continuous F f" and "continuous F g"
1.75 +  shows "continuous F (\<lambda>x. inner (f x) (g x))"
1.76 +  using assms unfolding continuous_def by (rule tendsto_inner)
1.77 +
1.78 +lemma continuous_euclidean_component:
1.79 +  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. f x \$\$ i)"
1.80 +  unfolding continuous_def by (rule tendsto_euclidean_component)
1.81 +
1.82 +lemma continuous_inverse:
1.83 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
1.84 +  assumes "continuous F f" and "f (netlimit F) \<noteq> 0"
1.85 +  shows "continuous F (\<lambda>x. inverse (f x))"
1.86 +  using assms unfolding continuous_def by (rule tendsto_inverse)
1.87 +
1.88 +lemma continuous_at_within_inverse:
1.89 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
1.90 +  assumes "continuous (at a within s) f" and "f a \<noteq> 0"
1.91 +  shows "continuous (at a within s) (\<lambda>x. inverse (f x))"
1.92 +  using assms unfolding continuous_within by (rule tendsto_inverse)
1.93 +
1.94 +lemma continuous_at_inverse:
1.95 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
1.96 +  assumes "continuous (at a) f" and "f a \<noteq> 0"
1.97 +  shows "continuous (at a) (\<lambda>x. inverse (f x))"
1.98 +  using assms unfolding continuous_at by (rule tendsto_inverse)
1.99 +
1.100 +lemmas continuous_intros = continuous_at_id continuous_within_id
1.101 +  continuous_const continuous_dist continuous_norm continuous_infnorm
1.102 +  continuous_add continuous_minus continuous_diff
1.103 +  continuous_scaleR continuous_mult
1.104 +  continuous_inner continuous_euclidean_component
1.105 +  continuous_at_inverse continuous_at_within_inverse
1.107  text{* Same thing for setwise continuity. *}
1.109 +lemma continuous_on_id: "continuous_on s (\<lambda>x. x)"
1.110 +  unfolding continuous_on_def by (fast intro: tendsto_ident_at_within)
1.112  lemma continuous_on_const: "continuous_on s (\<lambda>x. c)"
1.113    unfolding continuous_on_def by (auto intro: tendsto_intros)
1.115 +lemma continuous_on_norm:
1.116 +  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. norm (f x))"
1.117 +  unfolding continuous_on_def by (fast intro: tendsto_norm)
1.119 +lemma continuous_on_infnorm:
1.120 +  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. infnorm (f x))"
1.121 +  unfolding continuous_on by (fast intro: tendsto_infnorm)
1.123  lemma continuous_on_minus:
1.124    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
1.125    shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. - f x)"
1.126 @@ -3412,8 +3480,18 @@
1.127    using bounded_linear_euclidean_component
1.128    by (rule bounded_linear.continuous_on)
1.130 +lemma continuous_on_inverse:
1.131 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
1.132 +  assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
1.133 +  shows "continuous_on s (\<lambda>x. inverse (f x))"
1.134 +  using assms unfolding continuous_on by (fast intro: tendsto_inverse)
1.136  text{* Same thing for uniform continuity, using sequential formulations. *}
1.138 +lemma uniformly_continuous_on_id:
1.139 + "uniformly_continuous_on s (\<lambda>x. x)"
1.140 +  unfolding uniformly_continuous_on_def by auto
1.142  lemma uniformly_continuous_on_const:
1.143   "uniformly_continuous_on s (\<lambda>x. c)"
1.144    unfolding uniformly_continuous_on_def by simp
1.145 @@ -3465,24 +3543,6 @@
1.146    using uniformly_continuous_on_add[of s f "\<lambda>x. - g x"]
1.147    using uniformly_continuous_on_neg[of s g] by auto
1.149 -text{* Identity function is continuous in every sense. *}
1.151 -lemma continuous_within_id:
1.152 - "continuous (at a within s) (\<lambda>x. x)"
1.153 -  unfolding continuous_within by (rule Lim_at_within [OF tendsto_ident_at])
1.155 -lemma continuous_at_id:
1.156 - "continuous (at a) (\<lambda>x. x)"
1.157 -  unfolding continuous_at by (rule tendsto_ident_at)
1.159 -lemma continuous_on_id:
1.160 - "continuous_on s (\<lambda>x. x)"
1.161 -  unfolding continuous_on_def by (auto intro: tendsto_ident_at_within)
1.163 -lemma uniformly_continuous_on_id:
1.164 - "uniformly_continuous_on s (\<lambda>x. x)"
1.165 -  unfolding uniformly_continuous_on_def by auto
1.167  text{* Continuity of all kinds is preserved under composition. *}
1.169  lemma continuous_within_topological:
1.170 @@ -3522,6 +3582,16 @@
1.171    thus ?thesis using assms unfolding uniformly_continuous_on_def by auto
1.172  qed
1.174 +lemmas continuous_on_intros = continuous_on_id continuous_on_const
1.175 +  continuous_on_compose continuous_on_norm continuous_on_infnorm
1.176 +  continuous_on_add continuous_on_minus continuous_on_diff
1.177 +  continuous_on_scaleR continuous_on_mult continuous_on_inverse
1.178 +  continuous_on_inner continuous_on_euclidean_component
1.179 +  uniformly_continuous_on_add uniformly_continuous_on_const
1.180 +  uniformly_continuous_on_id uniformly_continuous_on_compose
1.181 +  uniformly_continuous_on_cmul uniformly_continuous_on_neg
1.182 +  uniformly_continuous_on_sub
1.184  text{* Continuity in terms of open preimages. *}
1.186  lemma continuous_at_open:
1.187 @@ -3804,8 +3874,9 @@
1.188    fixes s :: "'a::real_normed_vector set"
1.189    assumes "open s"  shows "open((\<lambda>x. a + x) ` s)"
1.190  proof-
1.191 -  { fix x have "continuous (at x) (\<lambda>x. x - a)" using continuous_sub[of "at x" "\<lambda>x. x" "\<lambda>x. a"] continuous_at_id[of x] continuous_const[of "at x" a] by auto  }
1.192 -  moreover have "{x. x - a \<in> s}  = op + a ` s" apply auto unfolding image_iff apply(rule_tac x="x - a" in bexI) by auto
1.193 +  { fix x have "continuous (at x) (\<lambda>x. x - a)"
1.194 +      by (intro continuous_diff continuous_at_id continuous_const) }
1.195 +  moreover have "{x. x - a \<in> s} = op + a ` s" by force
1.196    ultimately show ?thesis using continuous_open_preimage_univ[of "\<lambda>x. x - a" s] using assms by auto
1.197  qed
1.199 @@ -3838,53 +3909,6 @@
1.200    thus "x \<in> interior (op + a ` s)" unfolding mem_interior using `e>0` by auto
1.201  qed
1.203 -text {* We can now extend limit compositions to consider the scalar multiplier. *}
1.205 -lemma continuous_vmul:
1.206 -  fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
1.207 -  shows "continuous net c ==> continuous net (\<lambda>x. c(x) *\<^sub>R v)"
1.208 -  unfolding continuous_def by (intro tendsto_intros)
1.210 -lemma continuous_mul:
1.211 -  fixes c :: "'a::metric_space \<Rightarrow> real"
1.212 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
1.213 -  shows "continuous net c \<Longrightarrow> continuous net f
1.214 -             ==> continuous net (\<lambda>x. c(x) *\<^sub>R f x) "
1.215 -  unfolding continuous_def by (intro tendsto_intros)
1.217 -lemmas continuous_intros = continuous_add continuous_vmul continuous_cmul
1.218 -  continuous_const continuous_sub continuous_at_id continuous_within_id continuous_mul
1.220 -lemmas continuous_on_intros = continuous_on_add continuous_on_const
1.221 -  continuous_on_id continuous_on_compose continuous_on_minus
1.222 -  continuous_on_diff continuous_on_scaleR continuous_on_mult
1.223 -  continuous_on_inner continuous_on_euclidean_component
1.224 -  uniformly_continuous_on_add uniformly_continuous_on_const
1.225 -  uniformly_continuous_on_id uniformly_continuous_on_compose
1.226 -  uniformly_continuous_on_cmul uniformly_continuous_on_neg
1.227 -  uniformly_continuous_on_sub
1.229 -text {* And so we have continuity of inverse. *}
1.231 -lemma continuous_inv:
1.232 -  fixes f :: "'a::metric_space \<Rightarrow> real"
1.233 -  shows "continuous net f \<Longrightarrow> f(netlimit net) \<noteq> 0
1.234 -           ==> continuous net (inverse o f)"
1.235 -  unfolding continuous_def using Lim_inv by auto
1.237 -lemma continuous_at_within_inv:
1.238 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_field"
1.239 -  assumes "continuous (at a within s) f" "f a \<noteq> 0"
1.240 -  shows "continuous (at a within s) (inverse o f)"
1.241 -  using assms unfolding continuous_within o_def
1.242 -  by (intro tendsto_intros)
1.244 -lemma continuous_at_inv:
1.245 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_field"
1.246 -  shows "continuous (at a) f \<Longrightarrow> f a \<noteq> 0
1.247 -         ==> continuous (at a) (inverse o f) "
1.248 -  using within_UNIV[THEN sym, of "at a"] using continuous_at_within_inv[of a UNIV] by auto
1.250  text {* Topological properties of linear functions. *}
1.252  lemma linear_lim_0:
1.253 @@ -3999,7 +4023,7 @@
1.255  text{* Continuity of inverse function on compact domain. *}
1.257 -lemma continuous_on_inverse:
1.258 +lemma continuous_on_inv:
1.259    fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
1.260      (* TODO: can this be generalized more? *)
1.261    assumes "continuous_on s f"  "compact s"  "\<forall>x \<in> s. g (f x) = x"
1.262 @@ -4090,17 +4114,6 @@
1.263    shows "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. \<forall>e>0. \<exists>d>0. (\<forall>x' \<in> s. norm(x' - x) < d --> abs(f x' - f x) < e))"
1.264    unfolding continuous_on_iff dist_norm by simp
1.266 -lemma continuous_at_norm: "continuous (at x) norm"
1.267 -  unfolding continuous_at by (intro tendsto_intros)
1.269 -lemma continuous_on_norm: "continuous_on s norm"
1.270 -unfolding continuous_on by (intro ballI tendsto_intros)
1.272 -lemma continuous_at_infnorm: "continuous (at x) infnorm"
1.273 -  unfolding continuous_at Lim_at o_def unfolding dist_norm
1.274 -  apply auto apply (rule_tac x=e in exI) apply auto
1.275 -  using order_trans[OF real_abs_sub_infnorm infnorm_le_norm, of _ x] by (metis xt1(7))
1.277  text {* Hence some handy theorems on distance, diameter etc. of/from a set. *}
1.279  lemma compact_attains_sup:
1.280 @@ -5219,7 +5232,7 @@
1.282  lemma homeomorphism_compact:
1.283    fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
1.284 -    (* class constraint due to continuous_on_inverse *)
1.285 +    (* class constraint due to continuous_on_inv *)
1.286    assumes "compact s" "continuous_on s f"  "f ` s = t"  "inj_on f s"
1.287    shows "\<exists>g. homeomorphism s t f g"
1.288  proof-
1.289 @@ -5242,12 +5255,12 @@
1.290    hence "g ` t = s" by auto
1.291    ultimately
1.292    show ?thesis unfolding homeomorphism_def homeomorphic_def
1.293 -    apply(rule_tac x=g in exI) using g and assms(3) and continuous_on_inverse[OF assms(2,1), of g, unfolded assms(3)] and assms(2) by auto
1.294 +    apply(rule_tac x=g in exI) using g and assms(3) and continuous_on_inv[OF assms(2,1), of g, unfolded assms(3)] and assms(2) by auto
1.295  qed
1.297  lemma homeomorphic_compact:
1.298    fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
1.299 -    (* class constraint due to continuous_on_inverse *)
1.300 +    (* class constraint due to continuous_on_inv *)
1.301    shows "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s
1.302            \<Longrightarrow> s homeomorphic t"
1.303    unfolding homeomorphic_def by (metis homeomorphism_compact)