union — Mathlib

English

If f has unit speed on Icc x y and on Icc y z, then f has unit speed on Icc x z.

Русский

Если у f единичная скорость на Icc(x,y) и на Icc(y,z), то на Icc(x,z) тоже единичная скорость.

LaTeX

$$HasUnitSpeedOn f (Icc x y) → HasUnitSpeedOn f (Icc y z) → HasUnitSpeedOn f (Icc x z)$$

Lean4

theorem union {t : Set ℝ} {x : ℝ} (hfs : HasUnitSpeedOn f s) (hft : HasUnitSpeedOn f t) (hs : IsGreatest s x)
    (ht : IsLeast t x) : HasUnitSpeedOn f (s ∪ t) :=
  HasConstantSpeedOnWith.union hfs hft hs ht

Похожие утверждения