F. Riesz Theorem
In this article, we formalize in the Mizar system [1, 4] the F. Riesz theorem. In the first section, we defined Mizar functor ClstoCmp, compact topological spaces as closed interval subset of real numbers. Then using the former definition and referring to the article [10] and the article [5], we def...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Sciendo
2017-10-01
|
| Series: | Formalized Mathematics |
| Subjects: | |
| Online Access: | https://doi.org/10.1515/forma-2017-0017 |