hasConstantSpeedOnWith_of_subsingleton

English

If s is a subsingleton, then HasConstantSpeedOnWith f s l holds for any l (the speed is vacuously defined).

Русский

Если s подклетно, то HasConstantSpeedOnWith f s l выполняется для любого l (скорость тождественна нулю).

LaTeX

$$HasConstantSpeedOnWith f s l if s.Subsingleton$$

Lean4

theorem hasConstantSpeedOnWith_of_subsingleton (f : ℝ → E) {s : Set ℝ} (hs : s.Subsingleton) (l : ℝ≥0) :
    HasConstantSpeedOnWith f s l := by
  rintro x hx y hy; cases hs hx hy
  rw [eVariationOn.subsingleton f (fun y hy z hz => hs hy.1 hz.1 : (s ∩ Icc x x).Subsingleton)]
  simp only [sub_self, mul_zero, ENNReal.ofReal_zero]

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