equal
deleted
inserted
replaced
490 fix x assume x: "x \<in> F" |
490 fix x assume x: "x \<in> F" |
491 from a x have "g x = f x" .. |
491 from a x have "g x = f x" .. |
492 then have "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:) |
492 then have "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:) |
493 also from g_cont |
493 also from g_cont |
494 have "\<dots> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>" |
494 have "\<dots> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>" |
495 proof (rule fn_norm_le_cong [of g, folded B_def fn_norm_def]) |
495 proof (rule fn_norm_le_cong [OF _ linearformE, folded B_def fn_norm_def]) |
496 from FE x show "x \<in> E" .. |
496 from FE x show "x \<in> E" .. |
497 qed |
497 qed |
498 finally show "\<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>" . |
498 finally show "\<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>" . |
499 qed |
499 qed |
500 show "0 \<le> \<parallel>g\<parallel>\<hyphen>E" |
500 show "0 \<le> \<parallel>g\<parallel>\<hyphen>E" |