uniformContinuous' — Mathlib

English

A uniformly continuous p is continuous and can be characterized via basic neighborhoods in the uniform structure.

Русский

Равномерно непрерывная p определяется через базис окрестностей в униформной структуре.

LaTeX

$$$ \\text{UniformContinuous}(p) \\Rightarrow \\text{Continuous}(p). $$$

Lean4

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

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