uniformContinuous_of_forall' — Mathlib

English

If p is continuous at 0, then p is uniformly continuous (variant).

Русский

Если p непрерывна в нуле, тогда она равномерно непрерывна (вариант).

LaTeX

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

Lean4

/-- A seminorm is uniformly continuous if `p.closedBall 0 r ∈ 𝓝 0` for *all* `r > 0`.
Over a `NontriviallyNormedField` it is actually enough to check that this is true
for *some* `r`, see `Seminorm.uniformContinuous'`. -/
protected theorem uniformContinuous_of_forall' [UniformSpace E] [IsUniformAddGroup E] {p : Seminorm 𝕝 E}
    (hp : ∀ r > 0, p.closedBall 0 r ∈ (𝓝 0 : Filter E)) : UniformContinuous p :=
  Seminorm.uniformContinuous_of_continuousAt_zero (continuousAt_zero_of_forall' hp)

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