# F. Riesz Theorem

Keiko Narita; Kazuhisa Nakasho; Yasunari Shidama

Formalized Mathematics (2017)

- Volume: 25, Issue: 3, page 179-184
- ISSN: 1426-2630

## Access Full Article

top## Abstract

top## How to cite

topKeiko Narita, Kazuhisa Nakasho, and Yasunari Shidama. "F. Riesz Theorem." Formalized Mathematics 25.3 (2017): 179-184. <http://eudml.org/doc/288395>.

@article{KeikoNarita2017,

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].},

author = {Keiko Narita, Kazuhisa Nakasho, Yasunari Shidama},

journal = {Formalized Mathematics},

keywords = {F. Riesz theorem; dual spaces; continuous functions},

language = {eng},

number = {3},

pages = {179-184},

title = {F. Riesz Theorem},

url = {http://eudml.org/doc/288395},

volume = {25},

year = {2017},

}

TY - JOUR

AU - Keiko Narita

AU - Kazuhisa Nakasho

AU - Yasunari Shidama

TI - F. Riesz Theorem

JO - Formalized Mathematics

PY - 2017

VL - 25

IS - 3

SP - 179

EP - 184

AB - 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].

LA - eng

KW - F. Riesz theorem; dual spaces; continuous functions

UR - http://eudml.org/doc/288395

ER -

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.