uniformContinuousOn — Mathlib

English

If a function is K-Lipschitz on a set, it is uniformly continuous on that set.

Русский

Если функция липшицева на множества K, то она равномерно непрерывна на этом множестве.

LaTeX

$$$\\text{LipschitzOnWith } K f s \\Rightarrow \\text{ UniformContinuousOn } f s$$$

Lean4

protected theorem uniformContinuousOn (hf : LipschitzOnWith K f s) : UniformContinuousOn f s :=
  uniformContinuousOn_iff_restrict.mpr hf.to_restrict.uniformContinuous

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