<abstract xmlns="http://www.w3.org/1999/xhtml"><p>In this article, we formalize in the Mizar system [<xref ref-type="bibr" rid="j_forma-2017-0017_ref_001_w2aab3b7b1b1b6b1ab1ab1Aa">1</xref>, <xref ref-type="bibr" rid="j_forma-2017-0017_ref_004_w2aab3b7b1b1b6b1ab1ab4Aa">4</xref>] the F. Riesz theorem. In the first section, we defined Mizar functor <monospace>ClstoCmp</monospace>, compact topological spaces as closed interval subset of real numbers. Then using the former definition and referring to the article [<xref ref-type="bibr" rid="j_forma-2017-0017_ref_010_w2aab3b7b1b1b6b1ab1ac10Aa">10</xref>] and the article [<xref ref-type="bibr" rid="j_forma-2017-0017_ref_005_w2aab3b7b1b1b6b1ab1ab5Aa">5</xref>], we defined the normed spaces of continuous functions on closed interval subset of real numbers, and defined the normed spaces of bounded functions on closed interval subset of real numbers. We also proved some related properties.</p><p>In Sec.2, we proved some lemmas for the proof of F. Riesz theorem. In Sec.3, we proved F. Riesz theorem, about the dual space of the space of continuous functions on closed interval subset of real numbers, finally. We applied Hahn-Banach theorem (36) in [<xref ref-type="bibr" rid="j_forma-2017-0017_ref_007_w2aab3b7b1b1b6b1ab1ab7Aa">7</xref>], to the proof of the last theorem. For the description of theorems of this section, we also referred to the article [<xref ref-type="bibr" rid="j_forma-2017-0017_ref_008_w2aab3b7b1b1b6b1ab1ab8Aa">8</xref>] and the article [<xref ref-type="bibr" rid="j_forma-2017-0017_ref_006_w2aab3b7b1b1b6b1ab1ab6Aa">6</xref>]. These formalizations are based on [<xref ref-type="bibr" rid="j_forma-2017-0017_ref_002_w2aab3b7b1b1b6b1ab1ab2Aa">2</xref>], [<xref ref-type="bibr" rid="j_forma-2017-0017_ref_003_w2aab3b7b1b1b6b1ab1ab3Aa">3</xref>], [<xref ref-type="bibr" rid="j_forma-2017-0017_ref_009_w2aab3b7b1b1b6b1ab1ab9Aa">9</xref>], and [<xref ref-type="bibr" rid="j_forma-2017-0017_ref_011_w2aab3b7b1b1b6b1ab1ac11Aa">11</xref>].</p></abstract>

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 defined the normed spaces of continuous functions on closed interval subset of real numbers, and defined the normed spaces of bounded functions on closed interval subset of real numbers. We also proved some related properties.In Sec.2, we proved some lemmas for the proof of F. Riesz theorem. In Sec.3, we proved F. Riesz theorem, about the dual space of the space of continuous functions on closed interval subset of real numbers, finally. We applied Hahn-Banach theorem (36) in [7], to the proof of the last theorem. For the description of theorems of this section, we also referred to the article [8] and the article [6]. These formalizations are based on [2], [3], [9], and [11].

F. Riesz Theorem

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

{"article-title":"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...

F. Riesz Theorem

Publicado en línea: 19 dic 2017

Páginas: 179 - 184

Recibido: 30 ago 2017

DOI: https://doi.org/10.1515/forma-2017-0017

Palabras clave
F. Riesz theorem, dual spaces, continuous functions

© 2017 Keiko Narita et al., published by De Gruyter Open

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

F. Riesz Theorem

Publicado en línea: 19 dic 2017

Páginas: 179 - 184

Recibido: 30 ago 2017

DOI: https://doi.org/10.1515/forma-2017-0017

Palabras claveF. Riesz theorem, dual spaces, continuous functions

© 2017 Keiko Narita et al., published by De Gruyter Open

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Palabras clave
F. Riesz theorem, dual spaces, continuous functions