uniformContinuous — Mathlib

English

If p is continuous at 0, then p is uniformly continuous, provided a suitable uniform structure exists.

Русский

Если p непрерывна в 0, то она равномерно непрерывна при наличии подходящей униформной структуры.

LaTeX

$$$ (\\text{ContinuousAt}(p,0)) \\Rightarrow \\text{UniformContinuous}(p). $$$

Lean4

protected theorem uniformContinuous [UniformSpace E] [IsUniformAddGroup E] [ContinuousConstSMul 𝕜 E] {p : Seminorm 𝕜 E}
    {r : ℝ} (hp : p.ball 0 r ∈ (𝓝 0 : Filter E)) : UniformContinuous p :=
  Seminorm.uniformContinuous_of_continuousAt_zero (continuousAt_zero hp)

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