On the Properties of Curves and Parametrization-Independent Isoperimetric Inequality
Orcid profileDec 31, 2024
About this article
Published Online: Dec 31, 2024
Page range: 195 - 201
Accepted: Dec 14, 2024
DOI: https://doi.org/10.2478/forma-2024-0016
Keywords
© 2024 Kazuhisa Nakasho et al., published by Sciendo
This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 Public License.
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’s parametrization.