uniformContinuous — Mathlib

English

A Hölder function is uniformly continuous when the exponent r is positive.

Русский

Функция Холдер с положительным показательeм r является равномерно непрерывной.

LaTeX

$$$\text{UniformContinuous}(f) \quad\text{provided } r > 0$$$

Lean4

/-- A Hölder continuous function is uniformly continuous -/
protected theorem uniformContinuous (hf : HolderWith C r f) (h0 : 0 < r) : UniformContinuous f :=
  uniformContinuousOn_univ.mp <| (hf.holderOnWith univ).uniformContinuousOn h0

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