src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 56371 fb9ae0727548
parent 56290 801a72ad52d3
child 56541 0e3abadbef39
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Apr 02 18:35:02 2014 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Apr 02 18:35:07 2014 +0200
     1.3 @@ -791,7 +791,7 @@
     1.4  lemma open_ball [intro, simp]: "open (ball x e)"
     1.5  proof -
     1.6    have "open (dist x -` {..<e})"
     1.7 -    by (intro open_vimage open_lessThan continuous_on_intros)
     1.8 +    by (intro open_vimage open_lessThan continuous_intros)
     1.9    also have "dist x -` {..<e} = ball x e"
    1.10      by auto
    1.11    finally show ?thesis .
    1.12 @@ -2375,7 +2375,7 @@
    1.13  lemma closed_cball: "closed (cball x e)"
    1.14  proof -
    1.15    have "closed (dist x -` {..e})"
    1.16 -    by (intro closed_vimage closed_atMost continuous_on_intros)
    1.17 +    by (intro closed_vimage closed_atMost continuous_intros)
    1.18    also have "dist x -` {..e} = cball x e"
    1.19      by auto
    1.20    finally show ?thesis .
    1.21 @@ -4931,11 +4931,11 @@
    1.22  
    1.23  subsubsection {* Structural rules for setwise continuity *}
    1.24  
    1.25 -lemma continuous_on_infnorm[continuous_on_intros]:
    1.26 +lemma continuous_on_infnorm[continuous_intros]:
    1.27    "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. infnorm (f x))"
    1.28    unfolding continuous_on by (fast intro: tendsto_infnorm)
    1.29  
    1.30 -lemma continuous_on_inner[continuous_on_intros]:
    1.31 +lemma continuous_on_inner[continuous_intros]:
    1.32    fixes g :: "'a::topological_space \<Rightarrow> 'b::real_inner"
    1.33    assumes "continuous_on s f"
    1.34      and "continuous_on s g"
    1.35 @@ -4945,15 +4945,15 @@
    1.36  
    1.37  subsubsection {* Structural rules for uniform continuity *}
    1.38  
    1.39 -lemma uniformly_continuous_on_id[continuous_on_intros]:
    1.40 +lemma uniformly_continuous_on_id[continuous_intros]:
    1.41    "uniformly_continuous_on s (\<lambda>x. x)"
    1.42    unfolding uniformly_continuous_on_def by auto
    1.43  
    1.44 -lemma uniformly_continuous_on_const[continuous_on_intros]:
    1.45 +lemma uniformly_continuous_on_const[continuous_intros]:
    1.46    "uniformly_continuous_on s (\<lambda>x. c)"
    1.47    unfolding uniformly_continuous_on_def by simp
    1.48  
    1.49 -lemma uniformly_continuous_on_dist[continuous_on_intros]:
    1.50 +lemma uniformly_continuous_on_dist[continuous_intros]:
    1.51    fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space"
    1.52    assumes "uniformly_continuous_on s f"
    1.53      and "uniformly_continuous_on s g"
    1.54 @@ -4979,20 +4979,20 @@
    1.55      unfolding dist_real_def by simp
    1.56  qed
    1.57  
    1.58 -lemma uniformly_continuous_on_norm[continuous_on_intros]:
    1.59 +lemma uniformly_continuous_on_norm[continuous_intros]:
    1.60    assumes "uniformly_continuous_on s f"
    1.61    shows "uniformly_continuous_on s (\<lambda>x. norm (f x))"
    1.62    unfolding norm_conv_dist using assms
    1.63    by (intro uniformly_continuous_on_dist uniformly_continuous_on_const)
    1.64  
    1.65 -lemma (in bounded_linear) uniformly_continuous_on[continuous_on_intros]:
    1.66 +lemma (in bounded_linear) uniformly_continuous_on[continuous_intros]:
    1.67    assumes "uniformly_continuous_on s g"
    1.68    shows "uniformly_continuous_on s (\<lambda>x. f (g x))"
    1.69    using assms unfolding uniformly_continuous_on_sequentially
    1.70    unfolding dist_norm tendsto_norm_zero_iff diff[symmetric]
    1.71    by (auto intro: tendsto_zero)
    1.72  
    1.73 -lemma uniformly_continuous_on_cmul[continuous_on_intros]:
    1.74 +lemma uniformly_continuous_on_cmul[continuous_intros]:
    1.75    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    1.76    assumes "uniformly_continuous_on s f"
    1.77    shows "uniformly_continuous_on s (\<lambda>x. c *\<^sub>R f(x))"
    1.78 @@ -5004,12 +5004,12 @@
    1.79    shows "dist (- x) (- y) = dist x y"
    1.80    unfolding dist_norm minus_diff_minus norm_minus_cancel ..
    1.81  
    1.82 -lemma uniformly_continuous_on_minus[continuous_on_intros]:
    1.83 +lemma uniformly_continuous_on_minus[continuous_intros]:
    1.84    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    1.85    shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. - f x)"
    1.86    unfolding uniformly_continuous_on_def dist_minus .
    1.87  
    1.88 -lemma uniformly_continuous_on_add[continuous_on_intros]:
    1.89 +lemma uniformly_continuous_on_add[continuous_intros]:
    1.90    fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    1.91    assumes "uniformly_continuous_on s f"
    1.92      and "uniformly_continuous_on s g"
    1.93 @@ -5019,7 +5019,7 @@
    1.94    unfolding dist_norm tendsto_norm_zero_iff add_diff_add
    1.95    by (auto intro: tendsto_add_zero)
    1.96  
    1.97 -lemma uniformly_continuous_on_diff[continuous_on_intros]:
    1.98 +lemma uniformly_continuous_on_diff[continuous_intros]:
    1.99    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   1.100    assumes "uniformly_continuous_on s f"
   1.101      and "uniformly_continuous_on s g"
   1.102 @@ -5031,7 +5031,7 @@
   1.103  
   1.104  lemmas continuous_at_compose = isCont_o
   1.105  
   1.106 -lemma uniformly_continuous_on_compose[continuous_on_intros]:
   1.107 +lemma uniformly_continuous_on_compose[continuous_intros]:
   1.108    assumes "uniformly_continuous_on s f"  "uniformly_continuous_on (f ` s) g"
   1.109    shows "uniformly_continuous_on s (g \<circ> f)"
   1.110  proof -
   1.111 @@ -6972,7 +6972,7 @@
   1.112    apply (rule_tac x="\<lambda>x. c *\<^sub>R x" in exI)
   1.113    apply (rule_tac x="\<lambda>x. (1 / c) *\<^sub>R x" in exI)
   1.114    using assms
   1.115 -  apply (auto simp add: continuous_on_intros)
   1.116 +  apply (auto simp add: continuous_intros)
   1.117    done
   1.118  
   1.119  lemma homeomorphic_translation:
   1.120 @@ -7010,14 +7010,14 @@
   1.121      apply(rule_tac x="\<lambda>x. b + (e/d) *\<^sub>R (x - a)" in exI)
   1.122      apply(rule_tac x="\<lambda>x. a + (d/e) *\<^sub>R (x - b)" in exI)
   1.123      using assms
   1.124 -    apply (auto intro!: continuous_on_intros
   1.125 +    apply (auto intro!: continuous_intros
   1.126        simp: dist_commute dist_norm pos_divide_less_eq mult_strict_left_mono)
   1.127      done
   1.128    show ?cth unfolding homeomorphic_minimal
   1.129      apply(rule_tac x="\<lambda>x. b + (e/d) *\<^sub>R (x - a)" in exI)
   1.130      apply(rule_tac x="\<lambda>x. a + (d/e) *\<^sub>R (x - b)" in exI)
   1.131      using assms
   1.132 -    apply (auto intro!: continuous_on_intros
   1.133 +    apply (auto intro!: continuous_intros
   1.134        simp: dist_commute dist_norm pos_divide_le_eq mult_strict_left_mono)
   1.135      done
   1.136  qed