Functional Space Consisted by Continuous Functions on Topological Space

Hiroshi Yamazaki; Keiichi Miyajima; Yasunari Shidama

doi:10.2478/forma-2021-0005

.blurhash-client-img { display: none !important; }

Functional Space Consisted by Continuous Functions on Topological Space

Formalized Mathematics

Volume 29 (2021): Issue 1 (April 2021)

By: Hiroshi Yamazaki, Keiichi Miyajima and Yasunari Shidama

Open Access

|Aug 2021

Abstract

In this article, using the Mizar system [1], [2], first we give a definition of a functional space which is constructed from all continuous functions defined on a compact topological space [5]. We prove that this functional space is a Banach space [3]. Next, we give a definition of a function space which is constructed from all continuous functions with bounded support. We also prove that this function space is a normed space.

References

[1] Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8_17.10.1007/978-3-319-20615-8_17
Search in Google Scholar Back to article
[2] Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9–32, 2018. doi:10.1007/s10817-017-9440-6.10.1007/s10817-017-9440-6604425130069070
Search in Google Scholar Back to article
[3] Bruce K. Driver. Analysis Tools with Applications. Springer, Berlin, 2003.
Search in Google Scholar Back to article
[4] Takaya Nishiyama, Keiji Ohkubo, and Yasunari Shidama. The continuous functions on normed linear spaces. Formalized Mathematics, 12(3):269–275, 2004.
Search in Google Scholar Back to article
[5] Laurent Schwartz. Théorie des ensembles et topologie, tome 1. Analyse. Hermann, 1997.
Search in Google Scholar Back to article
[6] Yasumasa Suzuki. Banach space of bounded real sequences. Formalized Mathematics, 12 (2):77–83, 2004.
Search in Google Scholar Back to article
[7] Hiroshi Yamazaki. Functional sequence in norm space. Formalized Mathematics, 28(4): 263–268, 2020. doi:10.2478/forma-2020-0023.10.2478/forma-2020-0023
Search in Google Scholar Back to article

Articles in this issue

DOI: https://doi.org/10.2478/forma-2021-0005 | Journal eISSN: 1898-9934 | Journal ISSN: 1426-2630

Journal RSS Feed

Language: English

Page range: 49 - 62

Accepted on: Mar 30, 2021

Published on: Aug 26, 2021

Published by: University of Białystok

In partnership with: Paradigm Publishing Services

Publication frequency: 1 issue per year

Keywords:

continuous function space,

compact topological space,

Banach space

Related subjects:

Computer sciences,

Computer sciences, other,

Mathematics,

General mathematics

© 2021 Hiroshi Yamazaki, Keiichi Miyajima, Yasunari Shidama, published by University of Białystok
This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 License.

Volume 29 (2021): Issue 1 (April 2021)