<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

Online veröffentlicht: 21. Mai 2021

Seitenbereich: 263 - 268

Akzeptiert: 25. Okt. 2020

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

Schlüsselwörter
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

Online veröffentlicht: 21. Mai 2021

Seitenbereich: 263 - 268

Akzeptiert: 25. Okt. 2020

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

Schlüsselwörterpointwise 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.

Schlüsselwörter
pointwise convergence, functional sequence, formalized mathematics