F. Riesz Theorem

• Autorzy: Keiko Narita , Kazuhisa Nakasho , Yasunari Shidama
• 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

EN

F. Riesz theorem; dual spaces; continuous functions

Kategorie tematyczne

• 46E15: Banach spaces of continuous, differentiable or analytic functions
• 03B35: Mechanization of proofs and logical operations
• 46B10: Duality and reflexivity

• Wydawca: De Gruyter Open
• Czasopismo: Formalized Mathematics
• Rocznik: 2017
• Tom: 25
• Numer: 3
• Strony: 179-184

Daty

wydano

2017-10-01

otrzymano

2017-08-30

online

2017-12-19

Twórcy

autor

Keiko Narita

• Hirosaki-city, ,

autor

Kazuhisa Nakasho

• , ,

autor

Yasunari Shidama

• , ,

Identyfikatory

DOI

10.1515/forma-2017-0017