src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 44282 f0de18b62d63
parent 44252 10362a07eb7c
child 44286 8766839efb1b
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 18 17:42:35 2011 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 18 13:36:58 2011 -0700
     1.3 @@ -14,7 +14,7 @@
     1.4  
     1.5  lemma euclidean_dist_l2:"dist x (y::'a::euclidean_space) = setL2 (\<lambda>i. dist(x$$i) (y$$i)) {..<DIM('a)}"
     1.6    unfolding dist_norm norm_eq_sqrt_inner setL2_def apply(subst euclidean_inner)
     1.7 -  apply(auto simp add:power2_eq_square) unfolding euclidean_component.diff ..
     1.8 +  apply(auto simp add:power2_eq_square) unfolding euclidean_component_diff ..
     1.9  
    1.10  lemma dist_nth_le: "dist (x $$ i) (y $$ i) \<le> dist x (y::'a::euclidean_space)"
    1.11    apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)")
    1.12 @@ -1912,7 +1912,7 @@
    1.13    fixes S :: "'a::real_normed_vector set"
    1.14    shows "bounded S \<Longrightarrow> bounded ((\<lambda>x. c *\<^sub>R x) ` S)"
    1.15    apply (rule bounded_linear_image, assumption)
    1.16 -  apply (rule scaleR.bounded_linear_right)
    1.17 +  apply (rule bounded_linear_scaleR_right)
    1.18    done
    1.19  
    1.20  lemma bounded_translation:
    1.21 @@ -3537,7 +3537,7 @@
    1.22  proof-
    1.23    { fix x y assume "((\<lambda>n. f (x n) - f (y n)) ---> 0) sequentially"
    1.24      hence "((\<lambda>n. c *\<^sub>R f (x n) - c *\<^sub>R f (y n)) ---> 0) sequentially"
    1.25 -      using scaleR.tendsto [OF tendsto_const, of "(\<lambda>n. f (x n) - f (y n))" 0 sequentially c]
    1.26 +      using tendsto_scaleR [OF tendsto_const, of "(\<lambda>n. f (x n) - f (y n))" 0 sequentially c]
    1.27        unfolding scaleR_zero_right scaleR_right_diff_distrib by auto
    1.28    }
    1.29    thus ?thesis using assms unfolding uniformly_continuous_on_sequentially'
    1.30 @@ -4365,7 +4365,7 @@
    1.31    assumes "compact s"  shows "compact ((\<lambda>x. c *\<^sub>R x) ` s)"
    1.32  proof-
    1.33    let ?f = "\<lambda>x. scaleR c x"
    1.34 -  have *:"bounded_linear ?f" by (rule scaleR.bounded_linear_right)
    1.35 +  have *:"bounded_linear ?f" by (rule bounded_linear_scaleR_right)
    1.36    show ?thesis using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f]
    1.37      using linear_continuous_at[OF *] assms by auto
    1.38  qed
    1.39 @@ -4951,7 +4951,7 @@
    1.40          unfolding Lim_sequentially by(auto simp add: dist_norm)
    1.41        hence "(f ---> x) sequentially" unfolding f_def
    1.42          using tendsto_add[OF tendsto_const, of "\<lambda>n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x]
    1.43 -        using scaleR.tendsto [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] by auto  }
    1.44 +        using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] by auto  }
    1.45      ultimately have "x \<in> closure {a<..<b}"
    1.46        using as and open_interval_midpoint[OF assms] unfolding closure_def unfolding islimpt_sequential by(cases "x=?c")auto  }
    1.47    thus ?thesis using closure_minimal[OF interval_open_subset_closed closed_interval, of a b] by blast
    1.48 @@ -5571,7 +5571,7 @@
    1.49  subsection {* Some properties of a canonical subspace *}
    1.50  
    1.51  (** move **)
    1.52 -declare euclidean_component.zero[simp]  
    1.53 +declare euclidean_component_zero[simp]
    1.54  
    1.55  lemma subspace_substandard:
    1.56    "subspace {x::'a::euclidean_space. (\<forall>i<DIM('a). P i \<longrightarrow> x$$i = 0)}"
    1.57 @@ -6027,15 +6027,15 @@
    1.58  
    1.59  lemmas Lim_ident_at = LIM_ident
    1.60  lemmas Lim_const = tendsto_const
    1.61 -lemmas Lim_cmul = scaleR.tendsto [OF tendsto_const]
    1.62 +lemmas Lim_cmul = tendsto_scaleR [OF tendsto_const]
    1.63  lemmas Lim_neg = tendsto_minus
    1.64  lemmas Lim_add = tendsto_add
    1.65  lemmas Lim_sub = tendsto_diff
    1.66 -lemmas Lim_mul = scaleR.tendsto
    1.67 -lemmas Lim_vmul = scaleR.tendsto [OF _ tendsto_const]
    1.68 +lemmas Lim_mul = tendsto_scaleR
    1.69 +lemmas Lim_vmul = tendsto_scaleR [OF _ tendsto_const]
    1.70  lemmas Lim_null_norm = tendsto_norm_zero_iff [symmetric]
    1.71  lemmas Lim_linear = bounded_linear.tendsto [COMP swap_prems_rl]
    1.72 -lemmas Lim_component = euclidean_component.tendsto
    1.73 +lemmas Lim_component = tendsto_euclidean_component
    1.74  lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id
    1.75  
    1.76  end