<abstract xmlns="http://www.w3.org/1999/xhtml">

<p>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.</p>
</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.

Functional Space Consisted by Continuous Functions on Topological Space

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

{"article-title":"Functional Space Consisted by Continuous Functions on Topological Space"}

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

Functional Space Consisted by Continuous Functions on Topological Space

Published Online: Aug 26, 2021

Page range: 49 - 62

Accepted: Mar 30, 2021

DOI: https://doi.org/10.2478/forma-2021-0005

Keywords
continuous function space, compact topological space, Banach space

© 2021 Hiroshi Yamazaki et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Functional Space Consisted by Continuous Functions on Topological Space

Published Online: Aug 26, 2021

Page range: 49 - 62

Accepted: Mar 30, 2021

DOI: https://doi.org/10.2478/forma-2021-0005

Keywordscontinuous function space, compact topological space, Banach space

© 2021 Hiroshi Yamazaki et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Keywords
continuous function space, compact topological space, Banach space