REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

  1. Repozytorium Uniwersytetu w Białymstoku
  2. Czasopisma naukowe / Journals
  3. Formalized Mathematics
  4. Formalized Mathematics, 2022, Volume 30, Issue 3

Szukanie zaawansowane
  • Zespoły i Kolekcje


  • Zaloguj się
  • Zarejestruj się
  • Mój RUB
  • FAQ
  • Polityka
  • Regulamin
  • DOI
  • Instrukcja
  • Aspekty prawne
  • Open Access
  • Archiwum


  • Kontakt
  • O Dspace
  • Strona Biblioteki
  • Strona Uczelni



    • Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/14667
    Pełny rekord metadanych
    Pole DCWartośćJęzyk
    dc.contributor.authorNakasho, Kazuhisa-
    dc.contributor.authorShidama, Yasunari-
    dc.date.accessioned2023-02-15T09:29:06Z-
    dc.date.available2023-02-15T09:29:06Z-
    dc.date.issued2022-
    dc.identifier.citationFormalized Mathematics, Volume 30, Issue 3, Pages 159-168pl
    dc.identifier.issn1426-2630-
    dc.identifier.urihttp://hdl.handle.net/11320/14667-
    dc.description.abstractPrevious Mizar articles [7, 6, 5] formalized the implicit andinverse function theorems for Frechet continuously differentiable maps on Banachspaces. In this paper, using the Mizar system [1], [2], we formalize these theoremson Euclidean spaces by specializing them. We referred to [4], [12], [10], [11] in this formalization.pl
    dc.language.isoenpl
    dc.publisherDeGruyter Openpl
    dc.rightsAttribution-ShareAlike 3.0 Unported (CC BY-SA 3.0)pl
    dc.rightsCC BY-SA 3.0 licensepl
    dc.rights.urihttps://creativecommons.org/licenses/by-sa/3.0/pl
    dc.subjectimplicit function theorempl
    dc.subjectinverse function theorempl
    dc.subjectcontinuously differentiable functionpl
    dc.titleOn Implicit and Inverse Function Theorems on Euclidean Spacespl
    dc.typeArticlepl
    dc.rights.holder© 2022 The Author(s)pl
    dc.rights.holderCC BY-SA 3.0 licensepl
    dc.identifier.doi10.2478/forma-2022-0012-
    dc.description.AffiliationKazuhisa Nakasho - Yamaguchi University, Yamaguchi, Japanpl
    dc.description.AffiliationYasunari Shidama - Karuizawa Hotch 244-1, Nagano, Japanpl
    dc.description.referencesGrzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art andbeyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Vol-ker Sorge, editors, Intelligent Computer Mathematics, volume 9150 ofLecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615_817.pl
    dc.description.referencesGrzegorz 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.pl
    dc.description.referencesNoboru Endou, Yasunari Shidama, and Keiichi Miyajima. Partial differentiation on normed linear spaces Rⁿ. Formalized Mathematics, 15(2):65–72, 2007. doi:10.2478/v10037-007-0008-5.pl
    dc.description.referencesMiyadera Isao. Functional Analysis. Riko-Gaku-Sya, 1972.pl
    dc.description.referencesKazuhisa Nakasho and Yuichi Futa. Inverse function theorem. Part I. Formalized Mathematics, 29(1):9–19, 2021. doi:10.2478/forma-2021-0002pl
    dc.description.referencesKazuhisa Nakasho and Yasunari Shidama. Implicit function theorem. Part II. Formalized Mathematics, 27(2):117–131, 2019. doi:10.2478/forma-2019-0013.pl
    dc.description.referencesKazuhisa Nakasho, Yuichi Futa, and Yasunari Shidama. Implicit function theorem. Part I. Formalized Mathematics, 25(4):269–281, 2017. doi:10.1515/forma-2017-0026.pl
    dc.description.referencesKazuhisa Nakasho, Hiroyuki Okazaki, and Yasunari Shidama. Real vector space andrelated notions. Formalized Mathematics, 29(3):117–127, 2021. doi:10.2478/forma-2021-0012.pl
    dc.description.referencesHiroyuki Okazaki, Noboru Endou, and Yasunari Shidama. Cartesian products of familyof real linear spaces. Formalized Mathematics, 19(1):51–59, 2011. doi:10.2478/v10037-011-0009-2.pl
    dc.description.referencesLaurent Schwartz. Théorie des ensembles et topologie, tome 1. Analyse. Hermann, 1997.pl
    dc.description.referencesLaurent Schwartz. Calcul différentiel, tome 2. Analyse. Hermann, 1997.pl
    dc.description.referencesKôsaku Yosida.Functional Analysis. Springer, 1980.pl
    dc.identifier.eissn1898-9934-
    dc.description.volume30pl
    dc.description.issue3pl
    dc.description.firstpage159pl
    dc.description.lastpage168pl
    dc.identifier.citation2Formalized Mathematicspl
    Występuje w kolekcji(ach):Formalized Mathematics, 2022, Volume 30, Issue 3

    Pliki w tej pozycji:
    Plik Opis RozmiarFormat 
    10.2478_forma-2022-0012.pdf286,79 kBAdobe PDFOtwórz
    Pokaż uproszczony widok rekordu Zobacz statystyki


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