English
If f and φ have unit speed on s and if φ maps s monotonically onto t with the right endpoints, then φ is a translation on s: φ(y) = y − x + φ(x) for all y ∈ s, where x is a point of s.
Русский
Если f и φ имеют единичную скорость на s и φ отображает s монотонно на t, то φ на s является сдвигом: φ(y) = y − x + φ(x) для всех y∈s, где x∈s.
LaTeX
$$unique_unit_speed {φ : Real → Real} (φm : MonotoneOn φ s) (hfφ : HasUnitSpeedOn (f ∘ φ) s) (hf : HasUnitSpeedOn f (φ '' s)) ⦃x : Real⦄ (xs : x ∈ s) : EqOn φ (fun y => y - x + φ x) s$$
Lean4
/-- `f` has unit speed on `s` if it is linearly parameterized by `l = 1` on `s`. -/
def HasUnitSpeedOn (f : ℝ → E) (s : Set ℝ) :=
HasConstantSpeedOnWith f s 1
