English
If f0 and f1 agree near x and x ∈ s, then LineDifferentiableWithinAt for f0 and f1 within s are equivalent.
Русский
Если f0 и f1 совпадают около x и x принадлежит s, тогда внутри s линейная дифференцируемость эквивалентна.
LaTeX
$$$(nhdsWithin x s).EventuallyEq f_{0} f_{1} \\land x \\in s \\Rightarrow \\mathrm{LineDifferentiableWithinAt}_{\\mathbb{K}}(f_{0},s;x,v) \\iff \\mathrm{LineDifferentiableWithinAt}_{\\mathbb{K}}(f_{1},s;x,v)$$$
Lean4
/-- Converse to the mean value inequality: if `f` is line differentiable at `x₀` and `C`-lipschitz
then its line derivative at `x₀` in the direction `v` has norm bounded by `C * ‖v‖`. -/
theorem le_of_lipschitz {f : E → F} {f' : F} {x₀ : E} (hf : HasLineDerivAt 𝕜 f f' x₀ v) {C : ℝ≥0}
(hlip : LipschitzWith C f) : ‖f'‖ ≤ C * ‖v‖ :=
hf.le_of_lipschitzOn univ_mem (lipschitzOnWith_univ.2 hlip)
