On the Properties of Curves and Parametrization-Independent Isoperimetric Inequality
oraz 31 gru 2024
O artykule
Data publikacji: 31 gru 2024
Zakres stron: 195 - 201
Przyjęty: 14 gru 2024
DOI: https://doi.org/10.2478/forma-2024-0016
Słowa kluczowe
© 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.