PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
2017 | 25 | 3 | 179-184
Tytuł artykułu

F. Riesz Theorem

Treść / Zawartość
Warianty tytułu
Języki publikacji
EN
Abstrakty
EN
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].
Słowa kluczowe
Wydawca
Rocznik
Tom
25
Numer
3
Strony
179-184
Opis fizyczny
Daty
wydano
2017-10-01
otrzymano
2017-08-30
online
2017-12-19
Twórcy
autor
  • Hirosaki-city, ,
  • , ,
  • , ,
Bibliografia
Typ dokumentu
Bibliografia
Identyfikatory
Identyfikator YADDA
bwmeta1.element.doi-10_1515_forma-2017-0017
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.