English
If a function is locally Lipschitz around a point, then it is continuous at that point.
Русский
Если функция локально липшицева в окрестности точки, то она непрерывна в этой точке.
LaTeX
$$$ \\forall y:\\alpha, \\ dist(y,x) < r \\Rightarrow \\ dist(f(y),f(x)) \\le K \\cdot dist(y,x) \\Rightarrow \\operatorname{ContinuousAt}(f,x) $$$
Lean4
/-- If a function is locally Lipschitz around a point, then it is continuous at this point. -/
theorem continuousAt_of_locally_lipschitz {f : α → β} {x : α} {r : ℝ} (hr : 0 < r) (K : ℝ)
(h : ∀ y, dist y x < r → dist (f y) (f x) ≤ K * dist y x) : ContinuousAt f x := by
-- We use `h` to squeeze `dist (f y) (f x)` between `0` and `K * dist y x`
refine
tendsto_iff_dist_tendsto_zero.2
(squeeze_zero' (Eventually.of_forall fun _ => dist_nonneg) (mem_of_superset (ball_mem_nhds _ hr) h) ?_)
-- Then show that `K * dist y x` tends to zero as `y → x`
refine (continuous_const.mul (continuous_id.dist continuous_const)).tendsto' _ _ ?_
simp
