Icc_Icc — Mathlib

English

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

Русский

Если 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 Icc_Icc {x y z : ℝ} (hfs : HasUnitSpeedOn f (Icc x y)) (hft : HasUnitSpeedOn f (Icc y z)) :
    HasUnitSpeedOn f (Icc x z) :=
  HasConstantSpeedOnWith.Icc_Icc hfs hft

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