REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

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

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/17786
    Pełny rekord metadanych
    Pole DCWartośćJęzyk
    dc.contributor.authorNakasho, Kazuhisa-
    dc.contributor.authorShidama, Yasunari-
    dc.date.accessioned2025-01-09T12:19:13Z-
    dc.date.available2025-01-09T12:19:13Z-
    dc.date.issued2024-
    dc.identifier.citationFormalized Mathematics, Volume 32, Issue 1, Pages 195–201pl
    dc.identifier.issn1426-2630-
    dc.identifier.urihttp://hdl.handle.net/11320/17786-
    dc.description.abstractIn this article we formalize in Mizar several properties of curves. We introduce the definition of the ArcLenP function and define arc length parametrization with its fundamental properties. Finally we prove an isoperimetric inequality that holds regardless of the curve’s parametrization.pl
    dc.language.isoenpl
    dc.publisherDeGruyter Openpl
    dc.rightsAttribution-ShareAlike 3.0 Unported (CC BY-SA 3.0)pl
    dc.rights.urihttps://creativecommons.org/licenses/by-sa/3.0/pl
    dc.subjectisoperimetric theorempl
    dc.subjectdifferential geometrypl
    dc.subjectparametric curvepl
    dc.titleOn the Properties of Curves and Parametrization-Independent Isoperimetric Inequalitypl
    dc.typeArticlepl
    dc.rights.holder© 2024 The Author(s)pl
    dc.rights.holderCC BY-SA 3.0 licensepl
    dc.identifier.doi10.2478/forma-2024-0016-
    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 and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8_17.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.referencesViktor Bl˚asjö. The isoperimetric problem. The American Mathematical Monthly, 112(6): 526–566, 2005.pl
    dc.description.referencesNoboru Endou. Differentiation on interval. Formalized Mathematics, 31(1):9–21, 2023. doi:10.2478/forma-2023-0002.pl
    dc.description.referencesNoboru Endou and Yasunari Shidama. Multidimensional measure space and integration. Formalized Mathematics, 31(1):181–192, 2023. doi:10.2478/forma-2023-0017.pl
    dc.description.referencesNoboru Endou, Katsumi Wasaki, and Yasunari Shidama. Definition of integrability for partial functions from R to R and integrability for continuous functions. Formalized Mathematics, 9(2):281–284, 2001.pl
    dc.description.referencesNoboru Endou, Yasunari Shidama, and Masahiko Yamazaki. Integrability and the integral of partial functions from R into R. Formalized Mathematics, 14(4):207–212, 2006. doi:10.2478/v10037-006-0023-y.pl
    dc.description.referencesAdam Grabowski. On the subcontinua of a real line. Formalized Mathematics, 11(3): 313–322, 2003.pl
    dc.description.referencesJohn Harrison. The HOL Light system reference. 2023. http://www.cl.cam.ac.uk/~jrh13/hol-light/reference.pdf.pl
    dc.description.referencesJohn Harrison. The isoperimetric inequality. 2023. Available online at https://github.com/jrh13/hol-light/blob/master/100/isoperimetric.ml.pl
    dc.description.referencesAndreas Hehl. The isoperimetric inequality. Proseminar Curves and Surfaces, Universitaet Tuebingen, Tuebingen, 2013.pl
    dc.description.referencesPeter David Lax. A short path to the shortest path. The American Mathematical Monthly, 102(2):158–159, 1995.pl
    dc.description.referencesKazuhisa Nakasho and Yasunari Shidama. Classical Isoperimetric Theorem. Formalized Mathematics, 32(1):187–194, 2024. doi:10.2478/forma-2024-0015.pl
    dc.description.referencesRobert Osserman. The isoperimetric inequality. Bulletin of American Mathematical Monthly, 6(84):1182–1238, 1978.pl
    dc.description.referencesAndrew N. Pressley. Elementary Differential Geometry. Springer Science & Business Media, 2010.pl
    dc.description.referencesAlan Siegel. An isoperimetric theorem in plane geometry. Discrete and Computational Geometry, 29(2):239–255, 2003. doi:10.1007/s00454-002-2809-1.pl
    dc.description.referencesMarten Straatsma. Towards formalising the isoperimetric theorem. BSc thesis, Radboud University Nijmegen, 2022.pl
    dc.description.referencesFreek Wiedijk. Formalizing 100 theorems. Available online at http://www.cs.ru.nl/~freek/100/.pl
    dc.identifier.eissn1898-9934-
    dc.description.volume32pl
    dc.description.issue1pl
    dc.description.firstpage195pl
    dc.description.lastpage201pl
    dc.identifier.citation2Formalized Mathematicspl
    dc.identifier.orcid0000-0003-1110-4342-
    Występuje w kolekcji(ach):Formalized Mathematics, 2024, Volume 32, Issue 1

    Pliki w tej pozycji:
    Plik Opis RozmiarFormat 
    On-the-Properties-of-Curves-and-ParametrizationIndependent-Isoperimetric-Inequality.pdf285,68 kBAdobe PDFOtwórz
    Pokaż uproszczony widok rekordu Zobacz statystyki


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