Dear all, We are pleased to announce some progress in porting multivariate analysis from HOL Light. Several new theories are available now in the distribution from the definition of finite Cartesian products, to linear algebra on euclidean spaces, determinants, and topology on R^n. The latter formalizes several notions like convergence nets, cauchy sequences, completeness, compactness, continuity, Banach's and Edelstein's fixed point theorems. The theories have more than 13K lines of proofs and some 1K lines of SML code and are getting bigger and bigger.
So far we have been very pragmatic as to move on as fast as possible. This lead to the fact that some notions are not as general or as "nice" as one wishes them to be. Brian has already made some interesting comments and made some changes. Any further comments and suggestions are highly welcome! Best wishes, Robert Himmelmann and Amine Chaieb
