author huffman Thu Sep 01 07:31:33 2011 -0700 (2011-09-01 ago) changeset 44646 a6047ddd9377 parent 44638 74fb317aaeb5 child 44647 e4de7750cdeb
```     1.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Sep 01 14:35:51 2011 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Sep 01 07:31:33 2011 -0700
1.3 @@ -2556,6 +2556,14 @@
1.4    show ?thesis unfolding norm_eq_sqrt_inner id_def .
1.5  qed
1.6
1.7 +lemma tendsto_infnorm [tendsto_intros]:
1.8 +  assumes "(f ---> a) F" shows "((\<lambda>x. infnorm (f x)) ---> infnorm a) F"
1.9 +proof (rule tendsto_compose [OF LIM_I assms])
1.10 +  fix r :: real assume "0 < r"
1.11 +  thus "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (infnorm x - infnorm a) < r"
1.12 +    by (metis real_norm_def le_less_trans real_abs_sub_infnorm infnorm_le_norm)
1.13 +qed
1.14 +
1.15  text {* Equality in Cauchy-Schwarz and triangle inequalities. *}
1.16
1.17  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")
```