| changeset 22931 | 11cc1ccad58e |
| parent 19984 | 29bb4659f80a |
| child 23378 | 1d138d6bb461 |
| 22930:f99617e7103f | 22931:11cc1ccad58e |
|---|---|
264 from x_neq and x have "\<parallel>x\<parallel> \<noteq> 0" by simp |
264 from x_neq and x have "\<parallel>x\<parallel> \<noteq> 0" by simp |
265 then show ?thesis by simp |
265 then show ?thesis by simp |
266 qed |
266 qed |
267 finally show ?thesis . |
267 finally show ?thesis . |
268 qed |
268 qed |
269 qed (simp_all! add: continuous_def) |
269 qed (insert `continuous V norm f`, simp_all add: continuous_def) |
270 |
270 |
271 end |
271 end |