English
If p is a seminorm on a space E and the closed balls around 0 with every radius r > 0 belong to the neighborhood 0, then p is continuous at 0.
Русский
Пусть p — семинорм на пространство E. Если для каждого r > 0 шар, ограниченный вокруг 0, принадлежит окрестности 0, то p непрерывна в 0.
LaTeX
$$$ \\forall r>0,\; p.\\overline{Ball}(0,r) \\in \\mathcal{N}_0 \\quad \\Rightarrow \\quad \\text{ContinuousAt}(p,0). $$$
Lean4
/-- A seminorm is continuous at `0` 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.continuousAt_zero'`. -/
theorem continuousAt_zero_of_forall' [TopologicalSpace E] {p : Seminorm 𝕝 E}
(hp : ∀ r > 0, p.closedBall 0 r ∈ (𝓝 0 : Filter E)) : ContinuousAt p 0 :=
by
simp_rw [Seminorm.closedBall_zero_eq_preimage_closedBall] at hp
rwa [ContinuousAt, Metric.nhds_basis_closedBall.tendsto_right_iff, map_zero]
