<abstract xmlns="http://www.w3.org/1999/xhtml"><p>In this article, using the Mizar system [2], [1], we discuss invertible operators on Banach spaces. In the first chapter, we formalized the theorem that denotes any operators that are close enough to an invertible operator are also invertible by using the property of Neumann series.</p><p>In the second chapter, we formalized the continuity of an isomorphism that maps an invertible operator on Banach spaces to its inverse. These results are used in the proof of the implicit function theorem. We referred to [3], [10], [6], [7] in this formalization.</p></abstract>

In this article, using the Mizar system [2], [1], we discuss invertible operators on Banach spaces. In the first chapter, we formalized the theorem that denotes any operators that are close enough to an invertible operator are also invertible by using the property of Neumann series.In the second chapter, we formalized the continuity of an isomorphism that maps an invertible operator on Banach spaces to its inverse. These results are used in the proof of the implicit function theorem. We referred to [3], [10], [6], [7] in this formalization.

Invertible Operators on Banach Spaces

Formalized Mathematics

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

{"article-title":"Invertible Operators on Banach Spaces"}

In this article, using the Mizar system [2], [1], we discuss invertible operators on Banach spaces. In the first chapter, we formalized the theorem that...

Invertible Operators on Banach Spaces

Pubblicato online: 20 lug 2019

Pagine: 107 - 115

Accettato: 27 mag 2019

DOI: https://doi.org/10.2478/forma-2019-0012

Parole chiave
Banach space, invertible operator, Neumann series, isomorphism of linear operator spaces

© 2019 Kazuhisa Nakasho, published by Sciendo

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

Invertible Operators on Banach Spaces

Pubblicato online: 20 lug 2019

Pagine: 107 - 115

Accettato: 27 mag 2019

DOI: https://doi.org/10.2478/forma-2019-0012

Parole chiaveBanach space, invertible operator, Neumann series, isomorphism of linear operator spaces

© 2019 Kazuhisa Nakasho, published by Sciendo

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

Parole chiave
Banach space, invertible operator, Neumann series, isomorphism of linear operator spaces