Anzeige
Erschienen in:
2013 | OriginalPaper | Buchkapitel
Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
verfasst von : Johannes Hölzl, Fabian Immler, Brian Huffman
Erschienen in: Interactive Theorem Proving
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
The theory of analysis in Isabelle/HOL derives from earlier formalizations that were limited to specific concrete types: ℝ, ℂ and ℝ
n
. Isabelle’s new analysis theory unifies and generalizes these earlier efforts. The improvements are centered on two primary contributions: a generic theory of limits based on filters, and a new hierarchy of type classes that includes various topological, metric, vector, and algebraic spaces. These let us apply many results in multivariate analysis to types which are not Euclidean spaces, such as the extended real numbers, bounded continuous functions, or finite maps.