English
If for every radius r>0, the ball p.ball 0 r belongs to 𝓝 0, then p is continuous at 0.
Русский
Если для каждого r>0 шар p.ball 0 r принадлежит 𝓝 0, то p непрерывна в 0.
LaTeX
$$$ \\forall r>0:\\; p.\\mathrm{ball}(0,r) \\in \\mathcal{N}_0 \\Rightarrow \\text{ContinuousAt}(p,0). $$$
Lean4
/-- A seminorm is continuous at `0` 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.continuousAt_zero'`. -/
theorem continuousAt_zero_of_forall [TopologicalSpace E] {p : Seminorm 𝕝 E}
(hp : ∀ r > 0, p.ball 0 r ∈ (𝓝 0 : Filter E)) : ContinuousAt p 0 :=
continuousAt_zero_of_forall' (fun r hr ↦ Filter.mem_of_superset (hp r hr) <| p.ball_subset_closedBall _ _)
