equal
deleted
inserted
replaced
1 (* Title : FrechetDeriv.thy |
1 (* Title : FrechetDeriv.thy |
2 ID : $Id$ |
|
3 Author : Brian Huffman |
2 Author : Brian Huffman |
4 *) |
3 *) |
5 |
4 |
6 header {* Frechet Derivative *} |
5 header {* Frechet Derivative *} |
7 |
6 |
8 theory FrechetDeriv |
7 theory FrechetDeriv |
9 imports Lim |
8 imports Lim Complex_Main |
10 begin |
9 begin |
11 |
10 |
12 definition |
11 definition |
13 fderiv :: |
12 fderiv :: |
14 "['a::real_normed_vector \<Rightarrow> 'b::real_normed_vector, 'a, 'a \<Rightarrow> 'b] \<Rightarrow> bool" |
13 "['a::real_normed_vector \<Rightarrow> 'b::real_normed_vector, 'a, 'a \<Rightarrow> 'b] \<Rightarrow> bool" |