hasConstantSpeedOnWith_iff_ordered

English

HasConstantSpeedOnWith f s l is equivalent to a condition that for all x,y in s with x≤y, the variation on [x,y] equals l(y−x).

Русский

HasConstantSpeedOnWith f s l эквивалентно условию: для любых x,y в s с x≤y вариация на [x,y] равна l(y−x).

LaTeX

$$HasConstantSpeedOnWith f s l ⇔ ∀ x∈s, y∈s, x≤y → eVariationOn f (s∩Icc x y) = ENNReal.ofReal(l·(y−x))$$

Lean4

theorem hasConstantSpeedOnWith_iff_ordered :
    HasConstantSpeedOnWith f s l ↔
      ∀ ⦃x⦄ (_ : x ∈ s) ⦃y⦄ (_ : y ∈ s), x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (l * (y - x)) :=
  by
  refine ⟨fun h x xs y ys _ => h xs ys, fun h x xs y ys => ?_⟩
  rcases le_total x y with (xy | yx)
  · exact h xs ys xy
  · rw [eVariationOn.subsingleton, ENNReal.ofReal_of_nonpos]
    · exact mul_nonpos_of_nonneg_of_nonpos l.prop (sub_nonpos_of_le yx)
    · rintro z ⟨zs, xz, zy⟩ w ⟨ws, xw, wy⟩
      cases le_antisymm (zy.trans yx) xz
      cases le_antisymm (wy.trans yx) xw
      rfl

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