add lemma tendsto_infnorm
authorhuffman
Thu Sep 01 07:31:33 2011 -0700 (2011-09-01 ago)
changeset 44646a6047ddd9377
parent 44638 74fb317aaeb5
child 44647 e4de7750cdeb
add lemma tendsto_infnorm
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
     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")