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.4  
     1.5  text{* Combination results for pointwise continuity. *}
     1.6  
     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.40  
    1.41  lemma continuous_add:
    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.106  
   1.107  text{* Same thing for setwise continuity. *}
   1.108  
   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.111 +
   1.112  lemma continuous_on_const: "continuous_on s (\<lambda>x. c)"
   1.113    unfolding continuous_on_def by (auto intro: tendsto_intros)
   1.114  
   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.118 +
   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.122 +
   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.129  
   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.135 +
   1.136  text{* Same thing for uniform continuity, using sequential formulations. *}
   1.137  
   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.141 +
   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.148  
   1.149 -text{* Identity function is continuous in every sense. *}
   1.150 -
   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.154 -
   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.158 -
   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.162 -
   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.166 -
   1.167  text{* Continuity of all kinds is preserved under composition. *}
   1.168  
   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.173  
   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.183 +
   1.184  text{* Continuity in terms of open preimages. *}
   1.185  
   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.198  
   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.202  
   1.203 -text {* We can now extend limit compositions to consider the scalar multiplier. *}
   1.204 -
   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.209 -
   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.216 -
   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.219 -
   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.228 -
   1.229 -text {* And so we have continuity of inverse. *}
   1.230 -
   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.236 -
   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.243 -
   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.249 -
   1.250  text {* Topological properties of linear functions. *}
   1.251  
   1.252  lemma linear_lim_0:
   1.253 @@ -3999,7 +4023,7 @@
   1.254  
   1.255  text{* Continuity of inverse function on compact domain. *}
   1.256  
   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.265  
   1.266 -lemma continuous_at_norm: "continuous (at x) norm"
   1.267 -  unfolding continuous_at by (intro tendsto_intros)
   1.268 -
   1.269 -lemma continuous_on_norm: "continuous_on s norm"
   1.270 -unfolding continuous_on by (intro ballI tendsto_intros)
   1.271 -
   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.276 -
   1.277  text {* Hence some handy theorems on distance, diameter etc. of/from a set. *}
   1.278  
   1.279  lemma compact_attains_sup:
   1.280 @@ -5219,7 +5232,7 @@
   1.281  
   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.296  
   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)