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

<p>In this article, we formalize in Mizar [1], [2] functional sequences and basic operations on functional sequences in norm space based on [5]. In the first section, we define functional sequence in norm space. In the second section, we define pointwise convergence and prove some related theorems. In the last section we define uniform convergence and limit of functional sequence.</p>
</abstract>

In this article, we formalize in Mizar [1], [2] functional sequences and basic operations on functional sequences in norm space based on [5]. In the first section, we define functional sequence in norm space. In the second section, we define pointwise convergence and prove some related theorems. In the last section we define uniform convergence and limit of functional sequence.

Functional Sequence in Norm Space

Formalized Mathematics

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

{"article-title":"Functional Sequence in Norm Space"}

In this article, we formalize in Mizar [1], [2] functional sequences and basic operations on functional sequences in norm space based on [5]. In the first...

Functional Sequence in Norm Space

Published Online: May 21, 2021

Page range: 263 - 268

Accepted: Oct 25, 2020

DOI: https://doi.org/10.2478/forma-2020-0023

Keywords
pointwise convergence, functional sequence, formalized mathematics

© 2021 Hiroshi Yamazaki, published by Sciendo

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

Functional Sequence in Norm Space

Published Online: May 21, 2021

Page range: 263 - 268

Accepted: Oct 25, 2020

DOI: https://doi.org/10.2478/forma-2020-0023

Keywordspointwise convergence, functional sequence, formalized mathematics

© 2021 Hiroshi Yamazaki, published by Sciendo

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

Keywords
pointwise convergence, functional sequence, formalized mathematics