Assume I want to define length of plane curves axiomatically. It seems to be reasonable to assume that
- The length of a unit segment is 1;
- Congruent curves have equal lengths;
- Length is additive with respect to concatenation.
However this is not enuf to define length completely: many different length-like functionals satisfy these properties.
What would be a complete set of axioms?
Motivation. I noticed that many (if not all) proofs of the Crofton formula cheat by assuming implicitly that there is a unique length functional that satisfies the above property, which is wrong. The problem is easy to fix, but the proof I see relies on the constructive definition of length; therefore this extra argument has to be repeated in each variation of the Crofton formula, which is not nice.
P.S. It seems that the following set of axioms solves the problem (thanks to Taras Banakh):
- The length of any curve is non-negative and invariant with respect to reparametrizations.
- The length of a unit segment is 1;
- Congruent curves have equal lengths;
- Length is additive with respect to concatenation;
- Length is lower semi-continuous with respect to pointwise convergence.