changeset 61518 | ff12606337e9 |
parent 61306 | 9dd394c866fc |
child 61520 | 8f85bb443d33 |
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Sun Oct 25 17:31:14 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Mon Oct 26 23:41:27 2015 +0000 @@ -1507,6 +1507,8 @@ show "linear f" .. qed +lemmas linear_linear = linear_conv_bounded_linear[symmetric] + lemma linear_bounded_pos: fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector" assumes lf: "linear f"