equal
deleted
inserted
replaced
447 |
447 |
448 lemma bounded_linear_snd: "bounded_linear snd" |
448 lemma bounded_linear_snd: "bounded_linear snd" |
449 using snd_add snd_scaleR |
449 using snd_add snd_scaleR |
450 by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def) |
450 by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def) |
451 |
451 |
|
452 lemmas bounded_linear_fst_comp = bounded_linear_fst[THEN bounded_linear_compose] |
|
453 |
|
454 lemmas bounded_linear_snd_comp = bounded_linear_snd[THEN bounded_linear_compose] |
|
455 |
452 lemma bounded_linear_Pair: |
456 lemma bounded_linear_Pair: |
453 assumes f: "bounded_linear f" |
457 assumes f: "bounded_linear f" |
454 assumes g: "bounded_linear g" |
458 assumes g: "bounded_linear g" |
455 shows "bounded_linear (\<lambda>x. (f x, g x))" |
459 shows "bounded_linear (\<lambda>x. (f x, g x))" |
456 proof |
460 proof |