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.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
```