equal
deleted
inserted
replaced
1505 assume "bounded_linear f" |
1505 assume "bounded_linear f" |
1506 then interpret f: bounded_linear f . |
1506 then interpret f: bounded_linear f . |
1507 show "linear f" .. |
1507 show "linear f" .. |
1508 qed |
1508 qed |
1509 |
1509 |
|
1510 lemmas linear_linear = linear_conv_bounded_linear[symmetric] |
|
1511 |
1510 lemma linear_bounded_pos: |
1512 lemma linear_bounded_pos: |
1511 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector" |
1513 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector" |
1512 assumes lf: "linear f" |
1514 assumes lf: "linear f" |
1513 shows "\<exists>B > 0. \<forall>x. norm (f x) \<le> B * norm x" |
1515 shows "\<exists>B > 0. \<forall>x. norm (f x) \<le> B * norm x" |
1514 proof - |
1516 proof - |