--- a/NEWS Thu Aug 25 16:42:13 2011 -0700
+++ b/NEWS Thu Aug 25 16:50:55 2011 -0700
@@ -218,6 +218,7 @@
Lim_linear ~> bounded_linear.tendsto
Lim_component ~> tendsto_euclidean_component
Lim_component_cart ~> tendsto_vec_nth
+ Lim_inner ~> tendsto_inner [OF tendsto_const]
dot_lsum ~> inner_setsum_left
dot_rsum ~> inner_setsum_right
subset_interior ~> interior_mono
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Aug 25 16:42:13 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Aug 25 16:50:55 2011 -0700
@@ -5104,10 +5104,6 @@
finally show ?thesis .
qed
-lemma Lim_inner:
- assumes "(f ---> l) net" shows "((\<lambda>y. inner a (f y)) ---> inner a l) net"
- by (intro tendsto_intros assms)
-
lemma continuous_at_inner: "continuous (at x) (inner a)"
unfolding continuous_at by (intro tendsto_intros)