[isabelle-dev] Multivariate analysis in Isabelle/HOL
ac638 at cam.ac.uk
Fri Mar 6 12:45:33 CET 2009
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
Robert Himmelmann and Amine Chaieb
More information about the isabelle-dev