equal
deleted
inserted
replaced
20 linear forms: |
20 linear forms: |
21 *} |
21 *} |
22 |
22 |
23 locale continuous = var V + norm_syntax + linearform + |
23 locale continuous = var V + norm_syntax + linearform + |
24 assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" |
24 assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" |
|
25 |
|
26 declare continuous.intro [intro?] continuous_axioms.intro [intro?] |
25 |
27 |
26 lemma continuousI [intro]: |
28 lemma continuousI [intro]: |
27 includes norm_syntax + linearform |
29 includes norm_syntax + linearform |
28 assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" |
30 assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" |
29 shows "continuous V norm f" |
31 shows "continuous V norm f" |