W BIAŁYMSTOKU
Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/8130Pełny rekord metadanych
| Pole DC | Wartość | Język |
|---|---|---|
| dc.contributor.author | Nakasho, Kazuhisa | - |
| dc.date.accessioned | 2019-07-29T08:28:47Z | - |
| dc.date.available | 2019-07-29T08:28:47Z | - |
| dc.date.issued | 2019 | - |
| dc.identifier.citation | Formalized Mathematics, Volume 27, Issue 2, Pages 107 - 115 | - |
| dc.identifier.issn | 1426-2630 | - |
| dc.identifier.uri | http://hdl.handle.net/11320/8130 | - |
| dc.description.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. | - |
| dc.language.iso | en | - |
| dc.publisher | DeGruyter Open | - |
| dc.subject | Banach space | - |
| dc.subject | invertible operator | - |
| dc.subject | Neumann series | - |
| dc.subject | isomorphism of linear operator spaces | - |
| dc.subject | 47A05 | - |
| dc.subject | 47J07 | - |
| dc.subject | 68T99 | - |
| dc.subject | 03B35 | - |
| dc.title | Invertible Operators on Banach Spaces | - |
| dc.type | Article | - |
| dc.identifier.doi | 10.2478/forma-2019-0012 | - |
| dc.description.Affiliation | Yamaguchi University, Yamaguchi, Japan | - |
| dc.description.references | Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9–32, 2018. doi:10.1007/s10817-017-9440-6. | - |
| dc.description.references | Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191–198, 2015. doi:10.1007/s10817-015-9345-1. | - |
| dc.description.references | Miyadera Isao. Functional Analysis. Riko-Gaku-Sya, 1972. | - |
| dc.description.references | Kazuhisa Nakasho, Yuichi Futa, and Yasunari Shidama. Implicit function theorem. Part I. Formalized Mathematics, 25(4):269–281, 2017. doi:10.1515/forma-2017-0026. | - |
| dc.description.references | Hiroyuki Okazaki, Noboru Endou, and Yasunari Shidama. Cartesian products of family of real linear spaces. Formalized Mathematics, 19(1):51–59, 2011. doi:10.2478/v10037-011-0009-2. | - |
| dc.description.references | Laurent Schwartz. Théorie des ensembles et topologie, tome 1. Analyse. Hermann, 1997. | - |
| dc.description.references | Laurent Schwartz. Calcul différentiel, tome 2. Analyse. Hermann, 1997. | - |
| dc.description.references | Yasunari Shidama. Banach space of bounded linear operators. Formalized Mathematics, 12(1):39–48, 2004. | - |
| dc.description.references | Yasunari Shidama. The Banach algebra of bounded linear operators. Formalized Mathematics, 12(2):103–108, 2004. | - |
| dc.description.references | Kosaku Yoshida. Functional Analysis. Springer, 1980. | - |
| dc.identifier.eissn | 1898-9934 | - |
| dc.description.volume | 27 | - |
| dc.description.issue | 2 | - |
| dc.description.firstpage | 107 | - |
| dc.description.lastpage | 115 | - |
| dc.identifier.citation2 | Formalized Mathematics | - |
| dc.identifier.orcid | 0000-0003-1110-4342 | - |
| Występuje w kolekcji(ach): | Formalized Mathematics, 2019, Volume 27, Issue 2 | |
Pliki w tej pozycji:
| Plik | Opis | Rozmiar | Format | |
|---|---|---|---|---|
| forma_2019_27_2_003.pdf | 235,34 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL
