continuous — Mathlib

English

A locally Lipschitz function is continuous.

Русский

Локально липшицева функция непрерывна.

LaTeX

$$$\\forall f,\\ LocallyLipschitz f\\Rightarrow Continuous f$$$

Lean4

/-- A locally Lipschitz function is continuous. (The converse is false: for example,
$x ↦ \sqrt{x}$ is continuous, but not locally Lipschitz at 0.) -/
protected theorem continuous {f : α → β} (hf : LocallyLipschitz f) : Continuous f :=
  by
  rw [continuous_iff_continuousAt]
  intro x
  rcases (hf x) with ⟨K, t, ht, hK⟩
  exact (hK.continuousOn).continuousAt ht

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