# HG changeset patch
# User huffman
# Date 1314887493 25200
# Node ID a6047ddd93778037580f43c8ec962ab2680364f9
# Parent  74fb317aaeb547059180635410159097b7f98864
add lemma tendsto_infnorm

diff -r 74fb317aaeb5 -r a6047ddd9377 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Sep 01 14:35:51 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Sep 01 07:31:33 2011 -0700
@@ -2556,6 +2556,14 @@
   show ?thesis unfolding norm_eq_sqrt_inner id_def .
 qed
 
+lemma tendsto_infnorm [tendsto_intros]:
+  assumes "(f ---> a) F" shows "((\<lambda>x. infnorm (f x)) ---> infnorm a) F"
+proof (rule tendsto_compose [OF LIM_I assms])
+  fix r :: real assume "0 < r"
+  thus "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (infnorm x - infnorm a) < r"
+    by (metis real_norm_def le_less_trans real_abs_sub_infnorm infnorm_le_norm)
+qed
+
 text {* Equality in Cauchy-Schwarz and triangle inequalities. *}
 
 lemma norm_cauchy_schwarz_eq: "x \<bullet> y = norm x * norm y \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x" (is "?lhs \<longleftrightarrow> ?rhs")