Topological groups are blends of groups and topological spaces with the property that the multiplication and inversion operations are continuous functions. They frequently occur in mathematics and physics, e.g. in the form of Lie groups. We have developed a formalization of topological groups in the theorem prover Isabelle. It contains basic properties of topological groups as well as their uniform structures. The most notable formalized result is the Birkhoff-Kakutani theorem which gives a necessary and sufficient condition for the metrizability of a topological group. We also give examples for topological groups such as R^n, R^× and the general linear group GL_n(R) with its subgroups. In this thesis we present our formalization and describe the proof of Birkhoff-Kakutani in detail.     «

Topological groups are blends of groups and topological spaces with the property that the multiplication and inversion operations are continuous functions. They frequently occur in mathematics and physics, e.g. in the form of Lie groups. We have developed a formalization of topological groups in the theorem prover Isabelle. It contains basic properties of topological groups as well as their uniform structures. The most notable formalized result is the Birkhoff-Kakutani theorem which gives a...     »

Topologische Gruppen sind Gruppen mit einer topologischen Struktur, bezüglich derer Multiplikation und Inversion stetige Funktionen sind. Sie treten häufig in Mathematik und Physik auf, etwa in Form von Lie-Gruppen. Wir haben mithilfe des Beweisassistenten Isabelle eine Formalisierung topologischer Gruppen entwickelt. Sie enthält grundlegende Eigenschaften topologischer Gruppen sowie ihre uniformen Strukturen. Das wichtigste formalisierte Ergebnis ist der Satz von Birkhoff-Kakutani, welcher eine notwendige und hinreichende Bedingung für die Metrisierbarkeit einer topologischen Gruppe angibt. Es werden außerdem Beispiele für topologische Gruppen angeführt, darunter R^n, R^× und die allgemeine lineare Gruppe GL_n(R) mit ihren Untergruppen. Diese Arbeit beschreibt zunächst die Formalisierung und geht dann im Detail auf den Beweis von Birkhoff-Kakutani ein.     «

Topologische Gruppen sind Gruppen mit einer topologischen Struktur, bezüglich derer Multiplikation und Inversion stetige Funktionen sind. Sie treten häufig in Mathematik und Physik auf, etwa in Form von Lie-Gruppen. Wir haben mithilfe des Beweisassistenten Isabelle eine Formalisierung topologischer Gruppen entwickelt. Sie enthält grundlegende Eigenschaften topologischer Gruppen sowie ihre uniformen Strukturen. Das wichtigste formalisierte Ergebnis ist der Satz von Birkhoff-Kakutani, welcher ein...     »