REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/6292
Tytuł: F. Riesz Theorem
Autorzy: Narita, Keiko
Nakasho, Kazuhisa
Shidama, Yasunari
Słowa kluczowe: F. Riesz theorem
dual spaces
continuous functions
Data wydania: 2017
Data dodania: 8-lut-2018
Wydawca: DeGruyter Open
Źródło: Formalized Mathematics, Volume 25, Issue 3, Pages 179–184
Abstrakt: SummaryIn 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].
Afiliacja: Narita Keiko - Hirosaki-city, Aomori, Japan
Nakasho Kazuhisa - Akita Prefectural University, Akita, Japan
Shidama Yasunari - Shinshu University, Nagano, Japan
URI: http://hdl.handle.net/11320/6292
DOI: 10.1515/forma-2017-0017
ISSN: 1426-2630
e-ISSN: 1898-9934
Typ Dokumentu: Article
Występuje w kolekcji(ach):Formalized Mathematics, 2017, Volume 25, Issue 3

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
forma-2017-0017.pdf279,26 kBAdobe PDFOtwórz
Pokaż pełny widok rekordu Zobacz statystyki


Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons