Eintrag weiter verarbeiten
F. Riesz Theorem
Gespeichert in:
| Zeitschriftentitel: | Formalized Mathematics |
|---|---|
| Personen und Körperschaften: | , , |
| In: | Formalized Mathematics, 25, 2017, 3, S. 179-184 |
| Format: | E-Article |
| Sprache: | Englisch |
| veröffentlicht: |
Walter de Gruyter GmbH
|
| Schlagwörter: |
| author_facet |
Narita, Keiko Nakasho, Kazuhisa Shidama, Yasunari Narita, Keiko Nakasho, Kazuhisa Shidama, Yasunari |
|---|---|
| author |
Narita, Keiko Nakasho, Kazuhisa Shidama, Yasunari |
| spellingShingle |
Narita, Keiko Nakasho, Kazuhisa Shidama, Yasunari Formalized Mathematics F. Riesz Theorem Applied Mathematics Computational Mathematics |
| author_sort |
narita, keiko |
| spelling |
Narita, Keiko Nakasho, Kazuhisa Shidama, Yasunari 1898-9934 1426-2630 Walter de Gruyter GmbH Applied Mathematics Computational Mathematics http://dx.doi.org/10.1515/forma-2017-0017 <jats:title>Summary</jats:title> <jats:p>In this article, we formalize in the Mizar system [1, 4] the F. Riesz theorem. In the first section, we defined Mizar functor <jats:monospace>ClstoCmp</jats:monospace>, 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.</jats:p> <jats: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 [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].</jats:p> F. Riesz Theorem Formalized Mathematics |
| doi_str_mv |
10.1515/forma-2017-0017 |
| facet_avail |
Online Free |
| finc_class_facet |
Mathematik |
| format |
ElectronicArticle |
| fullrecord |
blob:ai-49-aHR0cDovL2R4LmRvaS5vcmcvMTAuMTUxNS9mb3JtYS0yMDE3LTAwMTc |
| id |
ai-49-aHR0cDovL2R4LmRvaS5vcmcvMTAuMTUxNS9mb3JtYS0yMDE3LTAwMTc |
| institution |
DE-D275 DE-Bn3 DE-Brt1 DE-Zwi2 DE-D161 DE-Gla1 DE-Zi4 DE-15 DE-Pl11 DE-Rs1 DE-105 DE-14 DE-Ch1 DE-L229 |
| imprint |
Walter de Gruyter GmbH, 2017 |
| imprint_str_mv |
Walter de Gruyter GmbH, 2017 |
| issn |
1898-9934 1426-2630 |
| issn_str_mv |
1898-9934 1426-2630 |
| language |
English |
| mega_collection |
Walter de Gruyter GmbH (CrossRef) |
| match_str |
narita2017friesztheorem |
| publishDateSort |
2017 |
| publisher |
Walter de Gruyter GmbH |
| recordtype |
ai |
| record_format |
ai |
| series |
Formalized Mathematics |
| source_id |
49 |
| title |
F. Riesz Theorem |
| title_unstemmed |
F. Riesz Theorem |
| title_full |
F. Riesz Theorem |
| title_fullStr |
F. Riesz Theorem |
| title_full_unstemmed |
F. Riesz Theorem |
| title_short |
F. Riesz Theorem |
| title_sort |
f. riesz theorem |
| topic |
Applied Mathematics Computational Mathematics |
| url |
http://dx.doi.org/10.1515/forma-2017-0017 |
| publishDate |
2017 |
| physical |
179-184 |
| description |
<jats:title>Summary</jats:title>
<jats:p>In this article, we formalize in the Mizar system [1, 4] the F. Riesz theorem. In the first section, we defined Mizar functor <jats:monospace>ClstoCmp</jats:monospace>, 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.</jats:p>
<jats: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 [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].</jats:p> |
| container_issue |
3 |
| container_start_page |
179 |
| container_title |
Formalized Mathematics |
| container_volume |
25 |
| format_de105 |
Article, E-Article |
| format_de14 |
Article, E-Article |
| format_de15 |
Article, E-Article |
| format_de520 |
Article, E-Article |
| format_de540 |
Article, E-Article |
| format_dech1 |
Article, E-Article |
| format_ded117 |
Article, E-Article |
| format_degla1 |
E-Article |
| format_del152 |
Buch |
| format_del189 |
Article, E-Article |
| format_dezi4 |
Article |
| format_dezwi2 |
Article, E-Article |
| format_finc |
Article, E-Article |
| format_nrw |
Article, E-Article |
| _version_ |
1792323855047458828 |
| geogr_code |
not assigned |
| last_indexed |
2024-03-01T11:40:27.218Z |
| geogr_code_person |
not assigned |
| openURL |
url_ver=Z39.88-2004&ctx_ver=Z39.88-2004&ctx_enc=info%3Aofi%2Fenc%3AUTF-8&rfr_id=info%3Asid%2Fvufind.svn.sourceforge.net%3Agenerator&rft.title=F.+Riesz+Theorem&rft.date=2017-10-01&genre=article&issn=1426-2630&volume=25&issue=3&spage=179&epage=184&pages=179-184&jtitle=Formalized+Mathematics&atitle=F.+Riesz+Theorem&aulast=Shidama&aufirst=Yasunari&rft_id=info%3Adoi%2F10.1515%2Fforma-2017-0017&rft.language%5B0%5D=eng |
| SOLR | |
| _version_ | 1792323855047458828 |
| author | Narita, Keiko, Nakasho, Kazuhisa, Shidama, Yasunari |
| author_facet | Narita, Keiko, Nakasho, Kazuhisa, Shidama, Yasunari, Narita, Keiko, Nakasho, Kazuhisa, Shidama, Yasunari |
| author_sort | narita, keiko |
| container_issue | 3 |
| container_start_page | 179 |
| container_title | Formalized Mathematics |
| container_volume | 25 |
| description | <jats:title>Summary</jats:title> <jats:p>In this article, we formalize in the Mizar system [1, 4] the F. Riesz theorem. In the first section, we defined Mizar functor <jats:monospace>ClstoCmp</jats:monospace>, 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.</jats:p> <jats: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 [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].</jats:p> |
| doi_str_mv | 10.1515/forma-2017-0017 |
| facet_avail | Online, Free |
| finc_class_facet | Mathematik |
| format | ElectronicArticle |
| format_de105 | Article, E-Article |
| format_de14 | Article, E-Article |
| format_de15 | Article, E-Article |
| format_de520 | Article, E-Article |
| format_de540 | Article, E-Article |
| format_dech1 | Article, E-Article |
| format_ded117 | Article, E-Article |
| format_degla1 | E-Article |
| format_del152 | Buch |
| format_del189 | Article, E-Article |
| format_dezi4 | Article |
| format_dezwi2 | Article, E-Article |
| format_finc | Article, E-Article |
| format_nrw | Article, E-Article |
| geogr_code | not assigned |
| geogr_code_person | not assigned |
| id | ai-49-aHR0cDovL2R4LmRvaS5vcmcvMTAuMTUxNS9mb3JtYS0yMDE3LTAwMTc |
| imprint | Walter de Gruyter GmbH, 2017 |
| imprint_str_mv | Walter de Gruyter GmbH, 2017 |
| institution | DE-D275, DE-Bn3, DE-Brt1, DE-Zwi2, DE-D161, DE-Gla1, DE-Zi4, DE-15, DE-Pl11, DE-Rs1, DE-105, DE-14, DE-Ch1, DE-L229 |
| issn | 1898-9934, 1426-2630 |
| issn_str_mv | 1898-9934, 1426-2630 |
| language | English |
| last_indexed | 2024-03-01T11:40:27.218Z |
| match_str | narita2017friesztheorem |
| mega_collection | Walter de Gruyter GmbH (CrossRef) |
| physical | 179-184 |
| publishDate | 2017 |
| publishDateSort | 2017 |
| publisher | Walter de Gruyter GmbH |
| record_format | ai |
| recordtype | ai |
| series | Formalized Mathematics |
| source_id | 49 |
| spelling | Narita, Keiko Nakasho, Kazuhisa Shidama, Yasunari 1898-9934 1426-2630 Walter de Gruyter GmbH Applied Mathematics Computational Mathematics http://dx.doi.org/10.1515/forma-2017-0017 <jats:title>Summary</jats:title> <jats:p>In this article, we formalize in the Mizar system [1, 4] the F. Riesz theorem. In the first section, we defined Mizar functor <jats:monospace>ClstoCmp</jats:monospace>, 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.</jats:p> <jats: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 [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].</jats:p> F. Riesz Theorem Formalized Mathematics |
| spellingShingle | Narita, Keiko, Nakasho, Kazuhisa, Shidama, Yasunari, Formalized Mathematics, F. Riesz Theorem, Applied Mathematics, Computational Mathematics |
| title | F. Riesz Theorem |
| title_full | F. Riesz Theorem |
| title_fullStr | F. Riesz Theorem |
| title_full_unstemmed | F. Riesz Theorem |
| title_short | F. Riesz Theorem |
| title_sort | f. riesz theorem |
| title_unstemmed | F. Riesz Theorem |
| topic | Applied Mathematics, Computational Mathematics |
| url | http://dx.doi.org/10.1515/forma-2017-0017 |