unique_unit_speed
theorem unique_unit_speed :
∀ {E : Type u_2} [inst : PseudoEMetricSpace E] {f : ℝ → E} {s : Set ℝ} {φ : ℝ → ℝ},
MonotoneOn φ s →
HasUnitSpeedOn (f ∘ φ) s → HasUnitSpeedOn f (φ '' s) → ∀ ⦃x : ℝ⦄, x ∈ s → Set.EqOn φ (fun y => y - x + φ x) s
The theorem `unique_unit_speed` states that, given a pseudometric space `E` and functions `f : ℝ → E` and `φ : ℝ → ℝ`, along with a set `s` of real numbers, if `φ` is monotonic on `s`, both `f` and `f ∘ φ` have unit speed on `t` and `s` respectively, and if `f` maintains unit speed on the image of `s` under `φ`, then `φ` is essentially a translation on `s`. In other words, for every `x` in `s`, the value of `φ` at any point in `s` equals that point minus `x` plus the value of `φ` at `x`. This theorem describes a certain unique property of functions with unit speed in the context of pseudometric spaces.
More concisely: Given a pseudometric space, a monotonic function φ between a set of real numbers and itself, and functions f and g such that f maintains unit speed on the image of s under φ, and f and f ∘ φ have unit speed on their respective domains s and ℝ, respectively, then φ is a translation on s.
|
unique_unit_speed_on_Icc_zero
theorem unique_unit_speed_on_Icc_zero :
∀ {E : Type u_2} [inst : PseudoEMetricSpace E] {f : ℝ → E} {s t : ℝ},
0 ≤ s →
0 ≤ t →
∀ {φ : ℝ → ℝ},
MonotoneOn φ (Set.Icc 0 s) →
φ '' Set.Icc 0 s = Set.Icc 0 t →
HasUnitSpeedOn (f ∘ φ) (Set.Icc 0 s) → HasUnitSpeedOn f (Set.Icc 0 t) → Set.EqOn φ id (Set.Icc 0 s)
The theorem, `unique_unit_speed_on_Icc_zero`, states that in a pseudo metric space, if a function `f` has a unit speed on the interval `[0, t]` and the composite function `f ∘ φ` also has a unit speed on the interval `[0, s]`, and if `φ` is a monotone function that maps the interval `[0, s]` onto the interval `[0, t]`, then `φ` is the identity function on the interval `[0, s]`. This means that for every point in the interval `[0, s]`, the value of `φ` is the same as the value of the identity function, which is the point itself.
More concisely: If in a pseudo metric space, functions `f` and `g = f ∘ φ` have unit speed on the intervals `[0, t]` and `[0, s]`, respectively, and `φ` is a monotone function mapping `[0, s]` onto `[0, t]`, then `φ` is the identity function on `[0, s]`.
|