English
If for every radius r>0 the closed ball around 0 is in the neighborhood of 0, then p is uniformly continuous.
Русский
Если для каждого радиуса r>0 замкнутый шар вокруг нуля лежит в окрестности нуля, то p является равномерно непрерывной.
LaTeX
$$$ (\\forall r>0,\; p.\\overline{Ball}(0,r) \\in 𝓝 0) \\Rightarrow \\text{UniformContinuous}(p). $$$
Lean4
/-- A seminorm is uniformly continuous if `p.ball 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.ball 0 r ∈ (𝓝 0 : Filter E)) : UniformContinuous p :=
Seminorm.uniformContinuous_of_continuousAt_zero (continuousAt_zero_of_forall hp)
