∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f : E → F} {a b : E} {C : ℝ} {s : Set E},
  IsOpen s →
    DiffContOnCl ℝ f s →
      openSegment ℝ a b ⊆ s →
        (∀ x ∈ s, ‖fderiv ℝ f x‖ ≤ C) →
          ‖f b - f a‖ ≤
            C * ‖b - a‖ * MeasureTheory.volume.real {t | t ∈ Set.Ioo 0 1 ∧ fderiv ℝ f ((AffineMap.lineMap a b) t) ≠ 0}