# 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 "((\x. infnorm (f x)) ---> infnorm a) F" +proof (rule tendsto_compose [OF LIM_I assms]) + fix r :: real assume "0 < r" + thus "\s>0. \x. x \ a \ norm (x - a) < s \ 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 \ y = norm x * norm y \ norm x *\<^sub>R y = norm y *\<^sub>R x" (is "?lhs \ ?rhs")