<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

Online veröffentlicht: 20. Juli 2019

Seitenbereich: 107 - 115

Akzeptiert: 27. Mai 2019

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

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

Online veröffentlicht: 20. Juli 2019

Seitenbereich: 107 - 115

Akzeptiert: 27. Mai 2019

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

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

Schlüsselwörter
Banach space, invertible operator, Neumann series, isomorphism of linear operator spaces