Implicit Function Theorem. Part II

Pole DC	Wartość	Język
dc.contributor.author	Nakasho, Kazuhisa	-
dc.contributor.author	Shidama, Yasunari	-
dc.date.accessioned	2019-07-29T08:28:48Z	-
dc.date.available	2019-07-29T08:28:48Z	-
dc.date.issued	2019	-
dc.identifier.citation	Formalized Mathematics, Volume 27, Issue 2, Pages 117 - 131	-
dc.identifier.issn	1426-2630	-
dc.identifier.uri	http://hdl.handle.net/11320/8131	-
dc.description.abstract	In this article, we formalize differentiability of implicit function theorem in the Mizar system [3], [1]. In the first half section, properties of Lipschitz continuous linear operators are discussed. Some norm properties of a direct sum decomposition of Lipschitz continuous linear operator are mentioned here.In the last half section, differentiability of implicit function in implicit function theorem is formalized. The existence and uniqueness of implicit function in [6] is cited. We referred to [10], [11], and [2] in the formalization.	-
dc.language.iso	en	-
dc.publisher	DeGruyter Open	-
dc.subject	implicit function theorem	-
dc.subject	Lipschitz continuity	-
dc.subject	differentiability	-
dc.subject	implicit function	-
dc.subject	26B10	-
dc.subject	47A05	-
dc.subject	47J07	-
dc.subject	53A07	-
dc.subject	03B35	-
dc.title	Implicit Function Theorem. Part II	-
dc.type	Article	-
dc.identifier.doi	10.2478/forma-2019-0013	-
dc.description.Affiliation	Kazuhisa Nakasho - Yamaguchi University, Yamaguchi, Japan	-
dc.description.Affiliation	Yasunari Shidama - Shinshu University, Nagano, 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	Bruce K. Driver. Analysis Tools with Applications. Springer, Berlin, 2003.	-
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	Hiroshi Imura, Morishige Kimura, and Yasunari Shidama. The differentiable functions on normed linear spaces. Formalized Mathematics, 12(3):321–327, 2004.	-
dc.description.references	Kazuhisa Nakasho. Invertible operators on Banach spaces. Formalized Mathematics, 27 (2):107–115, 2019. doi:10.2478/forma-2019-0012.	-
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	Takaya Nishiyama, Keiji Ohkubo, and Yasunari Shidama. The continuous functions on normed linear spaces. Formalized Mathematics, 12(3):269–275, 2004.	-
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	Hideki Sakurai, Hiroyuki Okazaki, and Yasunari Shidama. Banach’s continuous inverse theorem and closed graph theorem. Formalized Mathematics, 20(4):271–274, 2012. doi:10.2478/v10037-012-0032-y.	-
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.identifier.eissn	1898-9934	-
dc.description.volume	27	-
dc.description.issue	2	-
dc.description.firstpage	117	-
dc.description.lastpage	131	-
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_004.pdf		272,89 kB	Adobe PDF	Otwórz

Pokaż uproszczony widok rekordu Zobacz statystyki

Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL