<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

Data publikacji: 21 maj 2021

Zakres stron: 263 - 268

Przyjęty: 25 paź 2020

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

Słowa kluczowe
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

Data publikacji: 21 maj 2021

Zakres stron: 263 - 268

Przyjęty: 25 paź 2020

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

Słowa kluczowepointwise 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.

Słowa kluczowe
pointwise convergence, functional sequence, formalized mathematics