English
If a seminorm p is continuous in a neighborhood sense (via shells), then p is a continuous function.
Русский
Если семинормa непрерывна в окрестностях (через оболочки), то она непрерывна как функция.
LaTeX
$$$ \\exists\\; p:\\; \\text{Continuous}(p) \\ \\\\ \\text{iff}\\ \\forall r>0,\\ p.ball(0,r)\\in 𝓝 0. $$$
Lean4
/-- A seminorm is 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.continuous`. -/
protected theorem continuous_of_forall [TopologicalSpace E] [IsTopologicalAddGroup E] {p : Seminorm 𝕝 E}
(hp : ∀ r > 0, p.ball 0 r ∈ (𝓝 0 : Filter E)) : Continuous p :=
Seminorm.continuous_of_continuousAt_zero (continuousAt_zero_of_forall hp)
