English
A variant stating uniform continuity from a shell condition with prime notation.
Русский
Вариант равномерной непрерывности через условие оболочки c пометой ′.
LaTeX
$$$ \\text{uniformContinuity'}(p) \,\\text{следует из} \\, \\text{continuous'}(p). $$$
Lean4
/-- A seminorm is 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.continuous'`. -/
protected theorem continuous_of_forall' [TopologicalSpace E] [IsTopologicalAddGroup E] {p : Seminorm 𝕝 E}
(hp : ∀ r > 0, p.closedBall 0 r ∈ (𝓝 0 : Filter E)) : Continuous p :=
Seminorm.continuous_of_continuousAt_zero (continuousAt_zero_of_forall' hp)
