{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T12:59:31Z","timestamp":1777467571956,"version":"3.51.4"},"reference-count":18,"publisher":"Walter de Gruyter GmbH","issue":"1","license":[{"start":{"date-parts":[[2024,8,1]],"date-time":"2024-08-01T00:00:00Z","timestamp":1722470400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/3.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024,8,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n                  <jats:p>In 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\u2019s parametrization.<\/jats:p>","DOI":"10.2478\/forma-2024-0016","type":"journal-article","created":{"date-parts":[[2025,1,3]],"date-time":"2025-01-03T14:07:54Z","timestamp":1735913274000},"page":"195-201","source":"Crossref","is-referenced-by-count":0,"title":["On the Properties of Curves and Parametrization-Independent Isoperimetric Inequality"],"prefix":"10.2478","volume":"32","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1110-4342","authenticated-orcid":false,"given":"Kazuhisa","family":"Nakasho","sequence":"first","affiliation":[{"name":"Yamaguchi University , Yamaguchi , Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yasunari","family":"Shidama","sequence":"additional","affiliation":[{"name":"Karuizawa Hotch 244-1, Nagano , Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"374","published-online":{"date-parts":[[2024,12,31]]},"reference":[{"key":"2026042801390465369_j_forma-2024-0016_ref_001","doi-asserted-by":"crossref","unstructured":"Grzegorz Bancerek, Czes\u0142aw Byli\u0144ski, Adam Grabowski, Artur Korni\u0142owicz, Roman Matuszewski, Adam Naumowicz, Karol P\u0105k, 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\u2013279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007\/978-3-319-20615-8_17.","DOI":"10.1007\/978-3-319-20615-8_17"},{"key":"2026042801390465369_j_forma-2024-0016_ref_002","doi-asserted-by":"crossref","unstructured":"Grzegorz Bancerek, Czes\u0142aw Byli\u0144ski, Adam Grabowski, Artur Korni\u0142owicz, Roman Matuszewski, Adam Naumowicz, and Karol P\u0105k. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9\u201332, 2018. doi:10.1007\/s10817-017-9440-6.","DOI":"10.1007\/s10817-017-9440-6"},{"key":"2026042801390465369_j_forma-2024-0016_ref_003","doi-asserted-by":"crossref","unstructured":"Viktor Bl\u00e5sj\u00f6. The isoperimetric problem. The American Mathematical Monthly, 112(6): 526\u2013566, 2005.","DOI":"10.1080\/00029890.2005.11920227"},{"key":"2026042801390465369_j_forma-2024-0016_ref_004","doi-asserted-by":"crossref","unstructured":"Noboru Endou. Differentiation on interval. Formalized Mathematics, 31(1):9\u201321, 2023. doi:10.2478\/forma-2023-0002.","DOI":"10.2478\/forma-2023-0002"},{"key":"2026042801390465369_j_forma-2024-0016_ref_005","doi-asserted-by":"crossref","unstructured":"Noboru Endou and Yasunari Shidama. Multidimensional measure space and integration. Formalized Mathematics, 31(1):181\u2013192, 2023. doi:10.2478\/forma-2023-0017.","DOI":"10.2478\/forma-2023-0017"},{"key":"2026042801390465369_j_forma-2024-0016_ref_006","unstructured":"Noboru Endou, Katsumi Wasaki, and Yasunari Shidama. Definition of integrability for partial functions from \u211d to \u211d and integrability for continuous functions. Formalized Mathematics, 9(2):281\u2013284, 2001."},{"key":"2026042801390465369_j_forma-2024-0016_ref_007","doi-asserted-by":"crossref","unstructured":"Noboru Endou, Yasunari Shidama, and Masahiko Yamazaki. Integrability and the integral of partial functions from \u211d into \u211d. Formalized Mathematics, 14(4):207\u2013212, 2006. doi:10.2478\/v10037-006-0023-y.","DOI":"10.2478\/v10037-006-0023-y"},{"key":"2026042801390465369_j_forma-2024-0016_ref_008","unstructured":"Adam Grabowski. On the subcontinua of a real line. Formalized Mathematics, 11(3): 313\u2013322, 2003."},{"key":"2026042801390465369_j_forma-2024-0016_ref_009","unstructured":"John Harrison. The HOL Light system reference. 2023. http:\/\/www.cl.cam.ac.uk\/~jrh13\/hol-light\/reference.pdf."},{"key":"2026042801390465369_j_forma-2024-0016_ref_010","unstructured":"John Harrison. The isoperimetric inequality. 2023. Available online at https:\/\/github.com\/jrh13\/hol-light\/blob\/master\/100\/isoperimetric.ml."},{"key":"2026042801390465369_j_forma-2024-0016_ref_011","unstructured":"Andreas Hehl. The isoperimetric inequality. Proseminar Curves and Surfaces, Universitaet Tuebingen, Tuebingen, 2013."},{"key":"2026042801390465369_j_forma-2024-0016_ref_012","doi-asserted-by":"crossref","unstructured":"Peter David Lax. A short path to the shortest path. The American Mathematical Monthly, 102(2):158\u2013159, 1995.","DOI":"10.1080\/00029890.1995.11990550"},{"key":"2026042801390465369_j_forma-2024-0016_ref_013","doi-asserted-by":"crossref","unstructured":"Kazuhisa Nakasho and Yasunari Shidama. Classical Isoperimetric Theorem. Formalized Mathematics, 32(1):187\u2013194, 2024. doi:10.2478\/forma-2024-0015.","DOI":"10.2478\/forma-2024-0015"},{"key":"2026042801390465369_j_forma-2024-0016_ref_014","doi-asserted-by":"crossref","unstructured":"Robert Osserman. The isoperimetric inequality. Bulletin of American Mathematical Monthly, 6(84):1182\u20131238, 1978.","DOI":"10.1090\/S0002-9904-1978-14553-4"},{"key":"2026042801390465369_j_forma-2024-0016_ref_015","doi-asserted-by":"crossref","unstructured":"Andrew N. Pressley. Elementary Differential Geometry. Springer Science & Business Media, 2010.","DOI":"10.1007\/978-1-84882-891-9"},{"key":"2026042801390465369_j_forma-2024-0016_ref_016","doi-asserted-by":"crossref","unstructured":"Alan Siegel. An isoperimetric theorem in plane geometry. Discrete and Computational Geometry, 29(2):239\u2013255, 2003. doi:10.1007\/s00454-002-2809-1.","DOI":"10.1007\/s00454-002-2809-1"},{"key":"2026042801390465369_j_forma-2024-0016_ref_017","unstructured":"Marten Straatsma. Towards formalising the isoperimetric theorem. BSc thesis, Radboud University Nijmegen, 2022."},{"key":"2026042801390465369_j_forma-2024-0016_ref_018","unstructured":"Freek Wiedijk. Formalizing 100 theorems. Available online at http:\/\/www.cs.ru.nl\/~freek\/100\/."}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/reference-global.com\/pdf\/10.2478\/forma-2024-0016","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T13:31:15Z","timestamp":1777383075000},"score":1,"resource":{"primary":{"URL":"https:\/\/reference-global.com\/article\/10.2478\/forma-2024-0016"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,1]]},"references-count":18,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2024,12,31]]},"published-print":{"date-parts":[[2024,8,1]]}},"alternative-id":["10.2478\/forma-2024-0016"],"URL":"https:\/\/doi.org\/10.2478\/forma-2024-0016","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,8,1]]}}}